cryptol 2.13.0 → 3.0.0

raw patch · 105 files changed

+10640/−3132 lines, 105 filesdep +Win32dep +criterion-measurementdep +hgmpdep ~ghc-bignumdep ~sbvdep ~what4PVP ok

version bump matches the API change (PVP)

Dependencies added: Win32, criterion-measurement, hgmp, language-c99, language-c99-simple, libffi, pretty, pretty-show, unix, vector

Dependency ranges changed: ghc-bignum, sbv, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +100/−0
• bench/Main.hs +1/−2
• cryptol.cabal +45/−9
• cryptol/CheckExercises.hs +2/−1
• cryptol/Main.hs +1/−1
• lib/Array.cry +1/−0
• lib/Cryptol.cry +15/−5
• src/Cryptol/Backend/FFI.hs +276/−0
• src/Cryptol/Backend/FFI/Error.hs +44/−0
• src/Cryptol/Backend/FloatHelpers.hs +6/−0
• src/Cryptol/Backend/Monad.hs +27/−11
• src/Cryptol/Backend/What4.hs +1/−0
• src/Cryptol/Eval.hs +77/−10
• src/Cryptol/Eval/Concrete.hs +1/−7
• src/Cryptol/Eval/FFI.hs +430/−0
• src/Cryptol/Eval/FFI/GenHeader.hs +196/−0
• src/Cryptol/Eval/Generic.hs +16/−16
• src/Cryptol/Eval/Reference.lhs +26/−4
• src/Cryptol/Eval/SBV.hs +1/−0
• src/Cryptol/Eval/Type.hs +7/−1
• src/Cryptol/Eval/What4.hs +8/−10
• src/Cryptol/IR/FreeVars.hs +2/−0
• src/Cryptol/IR/TraverseNames.hs +267/−0
• src/Cryptol/ModuleSystem.hs +47/−11
• src/Cryptol/ModuleSystem/Base.hs +354/−148
• src/Cryptol/ModuleSystem/Binds.hs +434/−0
• src/Cryptol/ModuleSystem/Env.hs +209/−37
• src/Cryptol/ModuleSystem/Exports.hs +25/−19
• src/Cryptol/ModuleSystem/Fingerprint.hs +12/−0
• src/Cryptol/ModuleSystem/InstantiateModule.hs +0/−325
• src/Cryptol/ModuleSystem/Interface.hs +114/−78
• src/Cryptol/ModuleSystem/Monad.hs +88/−56
• src/Cryptol/ModuleSystem/Name.hs +155/−76
• src/Cryptol/ModuleSystem/Names.hs +88/−0
• src/Cryptol/ModuleSystem/NamingEnv.hs +167/−331
• src/Cryptol/ModuleSystem/Renamer.hs +708/−289
• src/Cryptol/ModuleSystem/Renamer/Error.hs +98/−42
• src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs +114/−0
• src/Cryptol/ModuleSystem/Renamer/Imports.hs +576/−0
• src/Cryptol/ModuleSystem/Renamer/Monad.hs +247/−80
• src/Cryptol/Parser.y +138/−81
• src/Cryptol/Parser/AST.hs +474/−76
• src/Cryptol/Parser/ExpandPropGuards.hs +137/−0
• src/Cryptol/Parser/Layout.hs +5/−1
• src/Cryptol/Parser/Lexer.x +2/−2
• src/Cryptol/Parser/Name.hs +5/−2
• src/Cryptol/Parser/Names.hs +17/−5
• src/Cryptol/Parser/NoInclude.hs +53/−14
• src/Cryptol/Parser/NoPat.hs +33/−32
• src/Cryptol/Parser/ParserUtils.hs +526/−50
• src/Cryptol/Parser/Position.hs +5/−0
• src/Cryptol/Parser/Token.hs +3/−1
• src/Cryptol/Parser/Unlit.hs +34/−2
• src/Cryptol/Parser/Utils.hs +2/−1
• src/Cryptol/REPL/Browse.hs +48/−19
• src/Cryptol/REPL/Command.hs +279/−224
• src/Cryptol/REPL/Help.hs +379/−0
• src/Cryptol/REPL/Monad.hs +67/−12
• src/Cryptol/Symbolic.hs +1/−1
• src/Cryptol/Symbolic/SBV.hs +19/−4
• src/Cryptol/Symbolic/What4.hs +41/−20
• src/Cryptol/Testing/Random.hs +29/−9
• src/Cryptol/Transform/AddModParams.hs +0/−314
• src/Cryptol/Transform/MonoValues.hs +11/−7
• src/Cryptol/Transform/Specialize.hs +21/−5
• src/Cryptol/TypeCheck.hs +3/−29
• src/Cryptol/TypeCheck/AST.hs +135/−35
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +0/−201
• src/Cryptol/TypeCheck/Default.hs +2/−0
• src/Cryptol/TypeCheck/Error.hs +188/−4
• src/Cryptol/TypeCheck/FFI.hs +112/−0
• src/Cryptol/TypeCheck/FFI/Error.hs +83/−0
• src/Cryptol/TypeCheck/FFI/FFIType.hs +70/−0
• src/Cryptol/TypeCheck/Infer.hs +441/−106
• src/Cryptol/TypeCheck/InferTypes.hs +12/−4
• src/Cryptol/TypeCheck/Interface.hs +57/−47
• src/Cryptol/TypeCheck/Kind.hs +44/−14
• src/Cryptol/TypeCheck/Module.hs +376/−0
• src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +408/−0
• src/Cryptol/TypeCheck/ModuleInstance.hs +168/−0
• src/Cryptol/TypeCheck/Monad.hs +402/−92
• src/Cryptol/TypeCheck/Parseable.hs +3/−0
• src/Cryptol/TypeCheck/Sanity.hs +209/−23
• src/Cryptol/TypeCheck/SimpType.hs +1/−0
• src/Cryptol/TypeCheck/Solve.hs +31/−9
• src/Cryptol/TypeCheck/Solver/Class.hs +1/−0
• src/Cryptol/TypeCheck/Solver/Improve.hs +2/−0
• src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +10/−0
• src/Cryptol/TypeCheck/Solver/SMT.hs +16/−4
• src/Cryptol/TypeCheck/Solver/Selector.hs +7/−7
• src/Cryptol/TypeCheck/Solver/Types.hs +1/−0
• src/Cryptol/TypeCheck/Subst.hs +79/−23
• src/Cryptol/TypeCheck/TCon.hs +1/−1
• src/Cryptol/TypeCheck/Type.hs +177/−14
• src/Cryptol/TypeCheck/TypeOf.hs +6/−1
• src/Cryptol/TypeCheck/TypePat.hs +7/−0
• src/Cryptol/Utils/Benchmark.hs +36/−0
• src/Cryptol/Utils/Fixity.hs +2/−2
• src/Cryptol/Utils/Ident.hs +145/−46
• src/Cryptol/Utils/PP.hs +64/−17
• src/Cryptol/Utils/Panic.hs +4/−1
• src/Cryptol/Utils/Patterns.hs +1/−0
• src/Cryptol/Utils/RecordMap.hs +7/−0
• src/Cryptol/Utils/Types.hs +10/−0
• src/Cryptol/Version.hs +4/−1

@@ -1,3 +1,103 @@+# 3.0.0 -- 2023-06-26++## Language changes++* Cryptol now includes a redesigned module system that is significantly more+  expressive than in previous releases. The new module system includes the+  following features:++  * Nested modules: Modules may now be defined within other modules.++  * Named interfaces: An interface specifies the parameters to a module.+    Separating the interface from the parameter declarations makes it possible+    to have different parameters that use the same interface.++  * Top-level module constraints: These are useful to specify constraints+    between different module parameters (i.e., ones that come from different+    interfaces or multiple copies of the same interface).++  See the+  [manual section](https://galoisinc.github.io/cryptol/master/Modules.html#instantiation-by-parametrizing-declarations)+  for more information.++* 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))+  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)+  for more information.++* The unary `-` operator now has the same precedence as binary `-`, meaning+  expressions like `-x^^2` will now parse as `-(x^^2)` instead of `(-x)^^2`.+  **This is a breaking change.** A warning has been added in cases where the+  behavior has changed, and can be disabled with `:set warnPrefixAssoc=off`.++* Infix operators are now allowed in import lists: `import M ((<+>))` will+  import only the operator `<+>` from module `M`.++* `lib/Array.cry` now contains an `arrayEq` primitive. Like the other+  array-related primitives, this has no computational interpretation (and+  therefore cannot be used in the Cryptol interpreter), but it is useful for+  stating specifications that are used in SAW.++## New features++* Add a `:time` command to benchmark the evaluation time of expressions.++* Add support for literate Cryptol using reStructuredText.  Cryptol code+  is extracted from `.. code-block:: cryptol` and `.. sourcecode:: cryptol`+  directives.++* Add a syntax highlight file for Vim,+  available in `syntax-highlight/cryptol.vim`++* Add `:new-seed` and `:set-seed` commands to the REPL.+  These affect random test generation,+  and help write reproducable Cryptol scripts.++* Add support for the CVC5 solver, which can be selected with+  `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can+  use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively. (Note that+  `sbv-cvc5` is non-functional on Windows at this time due to a downstream issue+  with CVC5 1.0.4 and earlier.)++* Add `:file-deps` commands to the REPL and Python API.+  It shows information about the source files and dependencies of+  modules or Cryptol files.++## Bug fixes++* Fix a bug in the What4 backend that could cause applications of `(@)` with+  symbolic `Integer` indices to become out of bounds (#1359).++* Fix a bug that caused finite bitvector enumerations to panic when used in+  combination with `(#)` (e.g., `[0..1] # 0`).++* Cryptol's markdown parser is slightly more permissive and will now parse code+  blocks with whitespace in between the backticks and `cryptol`. This sort of+  whitespace is often inserted by markdown generation tools such as `pandoc`.++* Improve documentation for `fromInteger` (#1465)++* Closed issues #812, #977, #1090, #1140, #1147, #1253, #1322, #1324, #1329,+  #1344, #1347, #1351, #1354, #1355, #1359, #1366, #1368, #1370, #1371, #1372,+  #1373, #1378, #1383, #1385, #1386, #1391, #1394, #1395, #1396, #1398, #1399,+  #1404, #1415, #1423, #1435, #1439, #1440, #1441, #1442, #1444, #1445, #1448,+  #1449, #1450, #1451, #1452, #1456, #1457, #1458, #1462, #1465, #1466, #1470,+  #1475, #1480, #1483, #1484, #1485, #1487, #1488, #1491, #1496, #1497, #1501,+  #1503, #1510, #1511, #1513, and #1514.++* Merged pull requests #1184, #1205, #1279, #1356, #1357, #1358, #1361, #1363,+  #1365, #1367, #1376, #1379, #1380, #1384, #1387, #1388, #1393, #1401, #1402,+  #1403, #1406, #1408, #1409, #1410, #1411, #1412, #1413, #1414, #1416, #1417,+  #1418, #1419, #1420, #1422, #1424, #1429, #1430, #1431, #1432, #1436, #1438,+  #1443, #1447, #1453, #1454, #1459, #1460, #1461, #1463, #1464, #1467, #1468,+  #1472, #1473, #1474, #1476, #1477, #1478, #1481, #1493, #1499, #1502, #1504,+  #1506, #1509, #1512, #1516, #1518, #1519, #1520, #1521, #1523, #1527, and+  #1528.+ # 2.13.0  ## Language changes

@@ -26,7 +26,6 @@ import qualified Cryptol.ModuleSystem.Env       as M import qualified Cryptol.ModuleSystem.Monad     as M import qualified Cryptol.ModuleSystem.NamingEnv as M-import           Cryptol.ModuleSystem.Interface (noIfaceParams)  import qualified Cryptol.Parser           as P import qualified Cryptol.Parser.AST       as P@@ -130,7 +129,7 @@                            , M.tcLinter = M.moduleLinter (P.thing (P.mName scm))                            , M.tcPrims  = prims                            }-      M.typecheck act scm noIfaceParams tcEnv+      M.typecheck act scm mempty tcEnv  ceval :: String -> String -> FilePath -> T.Text -> Benchmark ceval cd name path expr =

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             2.13.0+Version:             3.0.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@@ -9,11 +9,12 @@ Maintainer:          cryptol@galois.com Homepage:            http://www.cryptol.net/ Bug-reports:         https://github.com/GaloisInc/cryptol/issues-Copyright:           2013-2021 Galois Inc.+Copyright:           2013-2022 Galois Inc. Category:            Language Build-type:          Simple extra-source-files:  bench/data/*.cry                      CHANGES.md+                     lib/*.cry lib/*.z3  data-files:          **/*.cry **/*.z3 data-dir:            lib@@ -26,7 +27,7 @@   type:     git   location: https://github.com/GaloisInc/cryptol.git   -- add a tag on release branches-  tag:      2.13.0+  tag:      3.0.0   flag static@@ -37,6 +38,10 @@   default: True   description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution. +flag ffi+  default: True+  description: Enable the foreign function interface+ library   Default-language:     Haskell2010@@ -48,6 +53,7 @@                        bytestring        >= 0.10,                        array             >= 0.4,                        containers        >= 0.5,+                       criterion-measurement,                        cryptohash-sha1   >= 0.11 && < 0.12,                        deepseq           >= 1.3,                        directory         >= 1.2.2.0,@@ -57,30 +63,44 @@                        ghc-prim,                        GraphSCC          >= 1.0.4,                        heredoc           >= 0.2,+                       language-c99,+                       language-c99-simple,                        libBF             >= 0.6 && < 0.7,                        MemoTrie          >= 0.6 && < 0.7,                        monad-control     >= 1.0,                        monadLib          >= 3.7.2,                        parameterized-utils >= 2.0.2,+                       pretty,                        prettyprinter     >= 1.7.0,+                       pretty-show,                        process           >= 1.2,-                       sbv               >= 8.10 && < 9.1,+                       sbv               >= 9.1 && < 10.2,                        simple-smt        >= 0.9.7,                        stm               >= 2.4,                        strict,                        text              >= 1.1,                        tf-random         >= 0.5,                        transformers-base >= 0.4,+                       vector,                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.3 && < 1.4+                       what4             >= 1.4 && < 1.5    if impl(ghc >= 9.0)-    build-depends:     ghc-bignum        >= 1.0 && < 1.3+    build-depends:     ghc-bignum        >= 1.0 && < 1.4   else     build-depends:     integer-gmp       >= 1.0 && < 1.1 +  if flag(ffi)+    build-depends:     hgmp,+                       libffi            >= 0.2+    if os(windows)+      build-depends:   Win32+    else+      build-depends:   unix+    cpp-options:       -DFFI_ENABLED+   Build-tool-depends:  alex:alex, happy:happy   hs-source-dirs:      src @@ -93,6 +113,7 @@                        Cryptol.Parser.Names,                        Cryptol.Parser.Name,                        Cryptol.Parser.NoPat,+                       Cryptol.Parser.ExpandPropGuards,                        Cryptol.Parser.NoInclude,                        Cryptol.Parser.Selector,                        Cryptol.Parser.Utils,@@ -107,6 +128,8 @@                        Cryptol.Utils.Misc,                        Cryptol.Utils.Patterns,                        Cryptol.Utils.Logger,+                       Cryptol.Utils.Benchmark,+                       Cryptol.Utils.Types,                        Cryptol.Version,                         Cryptol.ModuleSystem,@@ -116,10 +139,13 @@                        Cryptol.ModuleSystem.Interface,                        Cryptol.ModuleSystem.Monad,                        Cryptol.ModuleSystem.Name,+                       Cryptol.ModuleSystem.Names,                        Cryptol.ModuleSystem.NamingEnv,+                       Cryptol.ModuleSystem.Binds                        Cryptol.ModuleSystem.Exports,-                       Cryptol.ModuleSystem.InstantiateModule,                        Cryptol.ModuleSystem.Renamer,+                       Cryptol.ModuleSystem.Renamer.Imports,+                       Cryptol.ModuleSystem.Renamer.ImplicitImports,                        Cryptol.ModuleSystem.Renamer.Monad,                        Cryptol.ModuleSystem.Renamer.Error, @@ -132,7 +158,6 @@                        Cryptol.TypeCheck.Parseable,                        Cryptol.TypeCheck.Monad,                        Cryptol.TypeCheck.Infer,-                       Cryptol.TypeCheck.CheckModuleInstance,                        Cryptol.TypeCheck.InferTypes,                        Cryptol.TypeCheck.Interface,                        Cryptol.TypeCheck.Error,@@ -147,6 +172,12 @@                        Cryptol.TypeCheck.TypeMap,                        Cryptol.TypeCheck.TypeOf,                        Cryptol.TypeCheck.Sanity,+                       Cryptol.TypeCheck.FFI,+                       Cryptol.TypeCheck.FFI.Error,+                       Cryptol.TypeCheck.FFI.FFIType,+                       Cryptol.TypeCheck.Module,+                       Cryptol.TypeCheck.ModuleInstance,+                       Cryptol.TypeCheck.ModuleBacktickInstance,                         Cryptol.TypeCheck.Solver.Types,                        Cryptol.TypeCheck.Solver.SMT,@@ -162,13 +193,15 @@                         Cryptol.Transform.MonoValues,                        Cryptol.Transform.Specialize,-                       Cryptol.Transform.AddModParams,                         Cryptol.IR.FreeVars,+                       Cryptol.IR.TraverseNames,                         Cryptol.Backend,                        Cryptol.Backend.Arch,                        Cryptol.Backend.Concrete,+                       Cryptol.Backend.FFI,+                       Cryptol.Backend.FFI.Error,                        Cryptol.Backend.FloatHelpers,                        Cryptol.Backend.Monad,                        Cryptol.Backend.SeqMap,@@ -179,6 +212,8 @@                        Cryptol.Eval,                        Cryptol.Eval.Concrete,                        Cryptol.Eval.Env,+                       Cryptol.Eval.FFI,+                       Cryptol.Eval.FFI.GenHeader,                        Cryptol.Eval.Generic,                        Cryptol.Eval.Prims,                        Cryptol.Eval.Reference,@@ -199,6 +234,7 @@                        Cryptol.Symbolic.What4,                         Cryptol.REPL.Command,+                       Cryptol.REPL.Help,                        Cryptol.REPL.Browse,                        Cryptol.REPL.Monad,                        Cryptol.REPL.Trie

@@ -291,7 +291,7 @@      if Seq.null (rdReplout rd)       then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))-              (cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""+              (cryEC, cryOut, cryErr) <- P.readCreateProcessWithExitCode cryCmd ""                 Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd@@ -301,6 +301,7 @@                   putStrLn $ "REPL error (replin lines " ++                     show lnReplinStart ++ "-" ++ show lnReplinEnd ++ ")."                   putStr cryOut+                  putStr cryErr                   exitFailure                 ExitSuccess -> do                   -- remove temporary input file

@@ -200,7 +200,7 @@             , "via the `:edit` command"             ]           )-        , ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"+        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"           , [ "A string of command-line arguments to be passed to the"             , "corresponding solver invoked for `:sat` and `:prove`"             , "when using a prover via SBV"

@@ -10,6 +10,7 @@ primitive arrayConstant : {a, b} b -> (Array a b) primitive arrayLookup : {a, b} (Array a b) -> a -> b primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)+primitive arrayEq : {n, a} (Array [n] a) -> (Array [n] a) -> Bool  /**  * Copy elements from the source array to the destination array.

@@ -339,11 +339,21 @@ primitive type Ring : * -> Prop  /**- * Converts an unbounded integer to a value in a Ring. When converting- * to the bitvector type [n], the value is reduced modulo 2^^n. Likewise,- * when converting to Z n, the value is reduced modulo n.  When converting- * to a floating-point value, the value is rounded to the nearest- * representable value.+ * Converts an unbounded integer to a value in a Ring using the following rules:+ *   * to bitvector type [n]:+ *     the value is reduced modulo 2^^n,+ *   * to Z n:+ *     the value is reduced modulo n,+ *   * floating point types:+ *     the value is rounded to the nearest representable value,+ *   * sequences other than bitvectors:+ *     elements are computed by using `fromInteger` pointwise+ *     Example: (fromInteger 2 : [3][8]) === [ 0x02, 0x02, 0x02 ]+ *   * tuples and records:+ *     elements are computed by using `fromInteger` pointwise+ *     Example: (fromInteger 2 : (Integer,[3][8])) === (2, [ 0x2, 0x2, 0x2 ])+ *   * functions:+ *     a constant function returning `fromInteger` on the result type  */ primitive fromInteger : {a} (Ring a) => Integer -> a 

@@ -0,0 +1,276 @@+{-# LANGUAGE BlockArguments            #-}+{-# LANGUAGE CPP                       #-}+{-# LANGUAGE DeriveAnyClass            #-}+{-# LANGUAGE DeriveGeneric             #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE LambdaCase                #-}+{-# LANGUAGE RecordWildCards           #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TypeApplications          #-}++-- | The implementation of loading and calling external functions from shared+-- libraries.+module Cryptol.Backend.FFI+  ( ForeignSrc+  , getForeignSrcPath+  , loadForeignSrc+  , unloadForeignSrc+  , foreignLibPath+#ifdef FFI_ENABLED+  , ForeignImpl+  , loadForeignImpl+  , FFIArg+  , FFIRet+  , SomeFFIArg (..)+  , callForeignImpl+#endif+  )+  where++import           Control.DeepSeq++import           Cryptol.Backend.FFI.Error++#ifdef FFI_ENABLED++import           Control.Concurrent.MVar+import           Control.Exception+import           Control.Monad+import           Data.Bifunctor+import           Data.Word+import           Foreign                    hiding (newForeignPtr)+import           Foreign.C.Types+import           Foreign.Concurrent+import           Foreign.LibFFI+import           System.FilePath            ((-<.>))+import           System.Directory(doesFileExist)+import           System.IO.Error+import           System.Info(os)++#if defined(mingw32_HOST_OS)+import           System.Win32.DLL+#else+import           System.Posix.DynamicLinker+#endif++import           Cryptol.Utils.Panic++#else++import           GHC.Generics++#endif++#ifdef FFI_ENABLED++-- | A source from which we can retrieve implementations of foreign functions.+data ForeignSrc = ForeignSrc+  { -- | The file path of the 'ForeignSrc'.+    foreignSrcPath   :: FilePath+    -- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the+    -- finalizer calls 'dlclose' when the library is no longer needed. We keep+    -- references to the 'ForeignPtr' in each foreign function that is in the+    -- evaluation environment, so that the shared library will stay open as long+    -- as there are references to it.+  , foreignSrcFPtr   :: ForeignPtr ()+    -- | We support explicit unloading of the shared library so we keep track of+    -- if it has already been unloaded, and if so the finalizer does nothing.+    -- This is updated atomically when the library is unloaded.+  , foreignSrcLoaded :: MVar Bool }++instance Show ForeignSrc where+  show = show . foreignSrcFPtr++instance NFData ForeignSrc where+  rnf ForeignSrc {..} = foreignSrcFPtr `seq` foreignSrcLoaded `deepseq` ()++-- | Get the file path of the 'ForeignSrc'.+getForeignSrcPath :: ForeignSrc -> Maybe FilePath+getForeignSrcPath = Just . foreignSrcPath++-- | Load a 'ForeignSrc' for the given __Cryptol__ file path. The file path of+-- the shared library that we try to load is the same as the Cryptol file path+-- except with a platform specific extension.+loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)+loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do+  foreignSrcLoaded <- newMVar True+  foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr)+  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+    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)++  where open libPath = do+#if defined(mingw32_HOST_OS)+          ptr <- loadLibrary libPath+#else+          -- RTLD_NOW so we can make sure that the symbols actually exist at+          -- module loading time+          ptr <- undl <$> dlopen libPath [RTLD_NOW]+#endif+          pure (libPath, ptr)++-- | Explicitly unload a 'ForeignSrc' immediately instead of waiting for the+-- garbage collector to do it. This can be useful if you want to immediately+-- load the same library again to pick up new changes.+--+-- The 'ForeignSrc' __must not__ be used in any way after this is called,+-- including calling 'ForeignImpl's loaded from it.+unloadForeignSrc :: ForeignSrc -> IO ()+unloadForeignSrc ForeignSrc {..} = withForeignPtr foreignSrcFPtr $+  unloadForeignSrc' foreignSrcLoaded++unloadForeignSrc' :: MVar Bool -> Ptr () -> IO ()+unloadForeignSrc' loaded lib = modifyMVar_ loaded \l -> do+  when l $ unloadForeignLib lib+  pure False++unloadForeignLib :: Ptr () -> IO ()+#if defined(mingw32_HOST_OS)+unloadForeignLib = freeLibrary+#else+unloadForeignLib = dlclose . DLHandle+#endif++withForeignSrc :: ForeignSrc -> (Ptr () -> IO a) -> IO a+withForeignSrc ForeignSrc {..} f = withMVar foreignSrcLoaded+  \case+    True -> withForeignPtr foreignSrcFPtr f+    False ->+      panic "[FFI] withForeignSrc" ["Use of foreign library after unload"]++-- | An implementation of a foreign function.+data ForeignImpl = ForeignImpl+  { foreignImplFun :: FunPtr ()+    -- | We don't need this to call the function but we want to keep the library+    -- around as long as we still have a function from it so that it isn't+    -- unloaded too early.+  , foreignImplSrc :: ForeignSrc+  }++-- | Load a 'ForeignImpl' with the given name from the given 'ForeignSrc'.+loadForeignImpl :: ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)+loadForeignImpl foreignImplSrc name =+  withForeignSrc foreignImplSrc \lib ->+    tryLoad (CantLoadFFIImpl name) do+      foreignImplFun <- loadForeignFunPtr lib name+      pure ForeignImpl {..}++loadForeignFunPtr :: Ptr () -> String -> IO (FunPtr ())+#if defined(mingw32_HOST_OS)+loadForeignFunPtr source symbol = do+  addr <- getProcAddress source symbol+  pure $ castPtrToFunPtr addr+#else+loadForeignFunPtr = dlsym . DLHandle+#endif++tryLoad :: (String -> FFILoadError) -> IO a -> IO (Either FFILoadError a)+tryLoad err = fmap (first $ err . displayException) . tryIOError++-- | Types which can be converted into libffi arguments.+--+-- The Storable constraint is so that we can put them in arrays.+class Storable a => FFIArg a where+  ffiArg :: a -> Arg++instance FFIArg Word8 where+  ffiArg = argWord8++instance FFIArg Word16 where+  ffiArg = argWord16++instance FFIArg Word32 where+  ffiArg = argWord32++instance FFIArg Word64 where+  ffiArg = argWord64++instance FFIArg CFloat where+  ffiArg = argCFloat++instance FFIArg CDouble where+  ffiArg = argCDouble++instance FFIArg (Ptr a) where+  ffiArg = argPtr++instance FFIArg CSize where+  ffiArg = argCSize++-- | Types which can be returned from libffi.+--+-- The Storable constraint is so that we can put them in arrays.+class Storable a => FFIRet a where+  ffiRet :: RetType a++instance FFIRet Word8 where+  ffiRet = retWord8++instance FFIRet Word16 where+  ffiRet = retWord16++instance FFIRet Word32 where+  ffiRet = retWord32++instance FFIRet Word64 where+  ffiRet = retWord64++instance FFIRet CFloat where+  ffiRet = retCFloat++instance FFIRet CDouble where+  ffiRet = retCDouble++instance FFIRet () where+  ffiRet = retVoid++-- | Existential wrapper around a 'FFIArg'.+data SomeFFIArg = forall a. FFIArg a => SomeFFIArg a++-- | Call a 'ForeignImpl' with the given arguments. The type parameter decides+-- how the return value should be converted into a Haskell value.+callForeignImpl :: forall a. FFIRet a => ForeignImpl -> [SomeFFIArg] -> IO a+callForeignImpl ForeignImpl {..} xs = withForeignSrc foreignImplSrc \_ ->+  callFFI foreignImplFun (ffiRet @a) $ map toArg xs+  where toArg (SomeFFIArg x) = ffiArg x++#else++data ForeignSrc = ForeignSrc deriving (Show, Generic, NFData)++getForeignSrcPath :: ForeignSrc -> Maybe FilePath+getForeignSrcPath _ = Nothing++loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)+loadForeignSrc _ = pure $ Right ForeignSrc++unloadForeignSrc :: ForeignSrc -> IO ()+unloadForeignSrc _ = pure ()++#endif

@@ -0,0 +1,44 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric  #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Safe  #-}++-- | Errors from dynamic loading of shared libraries for FFI.+module Cryptol.Backend.FFI.Error where++import           Control.DeepSeq+import           GHC.Generics++import           Cryptol.Utils.PP+import           Cryptol.ModuleSystem.Name++data FFILoadError+  = CantLoadFFISrc+    FilePath -- ^ Path to cryptol module+    String   -- ^ Error message+  | CantLoadFFIImpl+    String   -- ^ Function name+    String   -- ^ Error message+  | FFIDuplicates [Name]+  | FFIInFunctor  Name+  deriving (Show, Generic, NFData)++instance PP FFILoadError where+  ppPrec _ e =+    case e of+      CantLoadFFISrc path msg ->+        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)+      FFIDuplicates xs ->+        hang "Multiple foreign declarations with the same name:"+           4 (backticks (pp (nameIdent (head xs))) <+>+                 "defined at" <+> align (vcat (map (pp . nameLoc) xs)))+      FFIInFunctor x ->+        hang (pp (nameLoc x) <.> ":")+          4 "Foreign declaration" <+> backticks (pp (nameIdent x)) <+>+                "may not appear in a parameterized module."

@@ -8,6 +8,7 @@  import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic)+import Cryptol.Utils.Types import Cryptol.Backend.Monad( EvalError(..) )  @@ -176,3 +177,8 @@ -- (most significant bit in the significand is set, the rest of it is 0) floatToBits :: Integer -> Integer -> BigFloat -> Integer floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf+++-- | Create a 64-bit IEEE-754 float.+floatFromDouble :: Double -> BF+floatFromDouble = uncurry BF float64ExpPrec . bfFromDouble

@@ -54,7 +54,7 @@ import Cryptol.Parser.Position import Cryptol.Utils.Panic import Cryptol.Utils.PP-import Cryptol.TypeCheck.AST(Name)+import Cryptol.TypeCheck.AST(Name, TParam)  -- | A computation that returns an already-evaluated value. ready :: a -> Eval a@@ -412,16 +412,20 @@  -- | Data type describing errors that can occur during evaluation. data EvalError-  = InvalidIndex (Maybe Integer)  -- ^ Out-of-bounds index-  | DivideByZero                  -- ^ Division or modulus by 0-  | NegativeExponent              -- ^ Exponentiation by negative integer-  | LogNegative                   -- ^ Logarithm of a negative integer-  | UserError String              -- ^ Call to the Cryptol @error@ primitive-  | LoopError String              -- ^ Detectable nontermination-  | NoPrim Name                   -- ^ Primitive with no implementation-  | BadRoundingMode Integer       -- ^ Invalid rounding mode-  | BadValue String               -- ^ Value outside the domain of a partial function.-    deriving Typeable+  = InvalidIndex (Maybe Integer)         -- ^ Out-of-bounds index+  | DivideByZero                         -- ^ Division or modulus by 0+  | NegativeExponent                     -- ^ Exponentiation by negative integer+  | LogNegative                          -- ^ Logarithm of a negative integer+  | UserError String                     -- ^ Call to the Cryptol @error@ primitive+  | LoopError String                     -- ^ Detectable nontermination+  | NoPrim Name                          -- ^ Primitive with no implementation+  | 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.+  | FFINotSupported Name                 -- ^ Foreign function cannot be called+  | FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function+                                         --   as a type argument is too large+  deriving Typeable  instance PP EvalError where   ppPrec _ e = case e of@@ -440,6 +444,18 @@     BadRoundingMode r -> "invalid rounding mode" <+> integer r     BadValue x -> "invalid input for" <+> backticks (text x)     NoPrim x -> text "unimplemented primitive:" <+> pp x+    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."+      ]+    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`" ]  instance Show EvalError where   show = show . pp

@@ -11,6 +11,7 @@ {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} module Cryptol.Backend.What4 where 

@@ -15,6 +15,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NamedFieldPuns #-}  module Cryptol.Eval (     moduleEnv@@ -35,6 +36,7 @@   , Unsupported(..)   , WordTooWide(..)   , forceValue+  , checkProp   ) where  import Cryptol.Backend@@ -63,6 +65,7 @@ import qualified Data.IntMap.Strict as IntMap import qualified Data.Map.Strict as Map import           Data.Semigroup+import           Control.Applicative  import Prelude () import Prelude.Compat@@ -171,8 +174,9 @@       Just (Right val)         | ?callStacks ->             case nameInfo n of-              Declared{} -> sPushFrame sym n ?range (cacheCallStack sym =<< val)-              Parameter  -> cacheCallStack sym =<< val+              GlobalName {} ->+                 sPushFrame sym n ?range (cacheCallStack sym =<< val)+              LocalName {} -> cacheCallStack sym =<< val         | otherwise -> val       Nothing  -> do         envdoc <- ppEnv sym defaultPPOpts env@@ -215,13 +219,59 @@      env' <- evalDecls sym ds env      evalExpr sym env' e +  EPropGuards guards _ -> {-# SCC "evalExpr->EPropGuards" #-} do+    let checkedGuards = [ e | (ps,e) <- guards, all (checkProp . evalProp env) ps ]+    case checkedGuards of+      (e:_) -> eval e+      [] -> raiseError sym (NoMatchingPropGuardCase $ "Among constraint guards: " ++ show (fmap pp . fst <$> guards))+   where    {-# INLINE eval #-}   eval = evalExpr sym env   ppV = ppValue sym defaultPPOpts +-- | Checks whether an evaluated `Prop` holds+checkProp :: Prop -> Bool+checkProp = \case+  TCon tcon ts ->+    let ns = toNat' <$> ts in+    case tcon of+      PC PEqual | [n1, n2] <- ns -> n1 == n2+      PC PNeq | [n1, n2] <- ns -> n1 /= n2+      PC PGeq | [n1, n2] <- ns -> n1 >= n2+      PC PFin | [n] <- ns -> n /= Inf+      -- TODO: instantiate UniqueFactorization for Nat'?+      -- PC PPrime | [n] <- ns -> isJust (isPrime n) +      PC PTrue -> True+      TError {} -> False+      _ -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ TCon tcon ts ]+  prop -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ prop ]+  where+    toNat' :: Type -> Nat'+    toNat' = \case+      TCon (TC (TCNum n)) [] -> Nat n+      TCon (TC TCInf) [] -> Inf+      prop -> panic "checkProp" ["Expected `" ++ pretty prop ++ "` to be an evaluated numeric type"] ++-- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables according+-- to `envTypes` and expanding all type synonyms via `tNoUser`.+evalProp :: GenEvalEnv sym -> Prop -> Prop+evalProp env@EvalEnv { envTypes } = \case+  TCon tc tys+    | TError KProp <- tc, [p] <- tys ->+      case evalProp env p of+        x@(TCon (TError KProp) _) -> x+        _                         -> TCon (TError KProp) [evalProp env p]+    | otherwise -> TCon tc (toType . evalType envTypes <$> tys)+  TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty+  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+    toType = either tNumTy tValTy+ -- | Capure the current call stack from the evaluation monad and --   annotate function values.  When arguments are later applied --   to the function, the call stacks will be combined together.@@ -269,7 +319,7 @@   Newtype ->   GenEvalEnv sym ->   SEval sym (GenEvalEnv sym)-evalNewtypeDecl _sym nt = pure . bindVarDirect (ntName nt) (foldr tabs con (ntParams nt))+evalNewtypeDecl _sym nt = pure . bindVarDirect (ntConName nt) (foldr tabs con (ntParams nt))   where   con           = PFun PPrim @@ -382,9 +432,11 @@   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)]-    DExpr _ -> do+    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)   where@@ -407,8 +459,10 @@   GenEvalEnv sym  {- ^ An evaluation environment to extend with the given declaration -} ->   Decl            {- ^ The declaration to evaluate -} ->   SEval sym (GenEvalEnv sym)-evalDecl sym renv env d =-  let ?range = nameLoc (dName d) in+-- evalDecl sym renv env d =+--   let ?range = nameLoc (dName d) in+evalDecl sym renv env d = do+  let ?range = nameLoc (dName d)   case dDefinition d of     DPrim ->       case ?evalPrim =<< asPrim (dName d) of@@ -416,6 +470,18 @@         Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env         Nothing        -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env +    DForeign _ -> 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.+      case lookupVar (dName d) env of+        Just _  -> pure env+        Nothing -> bindVar sym (dName d)+          (raiseError sym $ FFINotSupported $ dName d) env+     DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env  @@ -689,5 +755,6 @@     where       f env =           case dDefinition d of-            DPrim   -> evalPanic "evalMatch" ["Unexpected local primitive"]-            DExpr e -> evalExpr sym env e+            DPrim      -> evalPanic "evalMatch" ["Unexpected local primitive"]+            DForeign _ -> evalPanic "evalMatch" ["Unexpected local foreign"]+            DExpr e    -> evalExpr sym env e

@@ -8,16 +8,10 @@  {-# LANGUAGE BangPatterns #-} {-# LANGUAGE BlockArguments #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternGuards #-} {-# LANGUAGE Rank2Types #-}-{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE ViewPatterns #-} module Cryptol.Eval.Concrete   ( module Cryptol.Backend.Concrete   , Value@@ -87,7 +81,7 @@            case res of              Left _ -> mismatch -- different fields              Right efs ->-               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts+               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts                 in pure (EApp f (ERec efs))        (TVTuple ts, VTuple tvs) ->

@@ -0,0 +1,430 @@+{-# LANGUAGE BangPatterns        #-}+{-# LANGUAGE BlockArguments      #-}+{-# LANGUAGE CPP                 #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE NamedFieldPuns      #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE RecordWildCards     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections       #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE ViewPatterns        #-}++-- | Evaluation of foreign functions.+module Cryptol.Eval.FFI+  ( findForeignDecls+  , evalForeignDecls+  ) where++import           Cryptol.Backend.FFI+import           Cryptol.Backend.FFI.Error+import           Cryptol.Eval+import           Cryptol.TypeCheck.AST+import           Cryptol.TypeCheck.FFI.FFIType++#ifdef FFI_ENABLED++import           Control.Exception(bracket_)+import           Data.Either+import           Data.Foldable+import           Data.IORef+import           Data.Proxy+import           Data.Ratio+import           Data.Traversable+import           Data.Word+import           Foreign+import           Foreign.C.Types+import           GHC.Float+import           LibBF                         (bfFromDouble, bfToDouble,+                                                pattern NearEven)+import           Numeric.GMP.Raw.Unsafe+import           Numeric.GMP.Utils++import           Cryptol.Backend+import           Cryptol.Backend.Concrete+import           Cryptol.Backend.FloatHelpers+import           Cryptol.Backend.Monad+import           Cryptol.Backend.SeqMap+import           Cryptol.Eval.Env+import           Cryptol.Eval.Prims+import           Cryptol.Eval.Type+import           Cryptol.Eval.Value+import           Cryptol.ModuleSystem.Name+import           Cryptol.Utils.Ident+import           Cryptol.Utils.RecordMap++#endif++#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.+evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->+  Eval (Either [FFILoadError] EvalEnv)+evalForeignDecls fsrc decls env = io do+  ePrims <- 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++-- | Generate a 'Prim' value representing the given foreign function, containing+-- all the code necessary to marshal arguments and return values and do the+-- actual FFI call.+foreignPrimPoly :: Name -> FFIFunType -> ForeignImpl -> Prim Concrete+foreignPrimPoly name fft impl = buildNumPoly (ffiTParams fft) mempty+  where -- Add type lambdas for the type parameters and build a type environment+        -- that we can look up later to compute e.g. array sizes.+        --+        -- Given [p1, p2, ..., pk] {}, returns+        -- PNumPoly \n1 -> PNumPoly \n2 -> ... PNumPoly \nk ->+        --   foreignPrim name fft impl {p1 = n1, p2 = n2, ..., pk = nk}+        buildNumPoly (tp:tps) tenv = PNumPoly \n ->+          buildNumPoly tps $ bindTypeVar (TVBound tp) (Left n) tenv+        buildNumPoly [] tenv = foreignPrim name fft impl tenv++-- | Methods for obtaining a return value. The producer of this type must supply+-- both 1) a polymorphic IO object directly containing a return value that the+-- consumer can instantiate at any 'FFIRet' type, and 2) an effectful function+-- that takes some output arguments and modifies what they are pointing at to+-- store a return value. The consumer can choose which one to use.+data GetRet = GetRet+  { getRetAsValue   :: forall a. FFIRet a => IO a+  , getRetAsOutArgs :: [SomeFFIArg] -> IO () }++-- | Operations needed for returning a basic reference type.+data BasicRefRet a = BasicRefRet+  { -- | Initialize the object before passing to foreign function.+    initBasicRefRet    :: Ptr a -> IO ()+    -- | Free the object after returning from foreign function and obtaining+    -- return value.+  , clearBasicRefRet   :: Ptr a -> IO ()+    -- | Convert the object to a Cryptol value.+  , marshalBasicRefRet :: a -> Eval (GenValue Concrete) }++-- | Generate the monomorphic part of the foreign 'Prim', given a 'TypeEnv'+-- containing all the type arguments we have already received.+foreignPrim :: Name -> FFIFunType -> ForeignImpl -> TypeEnv -> Prim Concrete+foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes []+  where++  -- Build up the 'Prim' function for the FFI call.+  --+  -- Given [t1, t2 ... tm] we return+  -- PStrict \v1 -> PStrict \v2 -> ... PStrict \vm -> PPrim $+  --   marshalArg t1 v1 \a1 ->+  --     marshalArg t2 v2 \a2 -> ... marshalArg tm vm \am ->+  --       marshalRet ffiRetType GetRet+  --         { getRetAsValue = callForeignImpl impl [n1, ..., nk, a1, ..., am]+  --         , getRetAsOutArgs = \[o1, ..., ol] ->+  --             callForeignImpl impl [n1, ..., nk, a1, ..., am, o1, ..., ol] }+  buildFun :: [FFIType] -> [(FFIType, GenValue Concrete)] -> Prim Concrete+  buildFun (argType:argTypes) typesAndVals = PStrict \val ->+    buildFun argTypes $ typesAndVals ++ [(argType, val)]+  buildFun [] typesAndVals = PPrim $+    marshalArgs typesAndVals \inArgs -> do+      tyArgs <- traverse marshalTyArg ffiTParams+      let tyInArgs = tyArgs ++ inArgs+      marshalRet ffiRetType GetRet+        { getRetAsValue = callForeignImpl impl tyInArgs+        , getRetAsOutArgs = callForeignImpl impl . (tyInArgs ++) }++  -- Look up the value of a type parameter in the type environment and marshal+  -- it.+  marshalTyArg :: TParam -> Eval SomeFFIArg+  marshalTyArg tp+    | n <= toInteger (maxBound :: CSize) =+      pure $ SomeFFIArg @CSize $ fromInteger n+    | otherwise = raiseError Concrete $ FFITypeNumTooBig name tp n+    where n = evalFinType $ TVar $ TVBound tp++  -- Marshal the given value as the given FFIType and call the given function+  -- with the results. A single Cryptol argument may correspond to any number of+  -- C arguments, so the callback takes a list.+  --+  -- NOTE: the result must be used only in the callback since it may have a+  -- limited lifetime (e.g. pointer returned by alloca).+  marshalArg ::+    FFIType ->+    GenValue Concrete ->+    ([SomeFFIArg] -> Eval a) ->+    Eval a++  marshalArg FFIBool val f = f [SomeFFIArg @Word8 (fromBool (fromVBit val))]++  marshalArg (FFIBasic (FFIBasicVal t)) val f =+    getMarshalBasicValArg t \doExport ->+    do arg <- doExport val+       f [SomeFFIArg arg]++  marshalArg (FFIBasic (FFIBasicRef t)) val f =+    getMarshalBasicRefArg t \doExport  ->+    -- Since we need to do Eval actions in an IO callback, we need to manually+    -- unwrap and wrap the Eval datatype+    Eval \stk ->+      doExport val \arg ->+        with arg \ptr ->+          runEval stk (f [SomeFFIArg ptr])++  marshalArg (FFIArray (map evalFinType -> sizes) bt) val f =+    case bt of++      FFIBasicVal t ->+        getMarshalBasicValArg t \doExport  ->+          -- Since we need to do Eval actions in an IO callback,+          -- we need to manually unwrap and wrap the Eval datatype+          Eval \stk ->+            marshalArrayArg stk \v k ->+              k =<< runEval stk (doExport v)++      FFIBasicRef t -> Eval \stk ->+        getMarshalBasicRefArg t \doExport ->+        marshalArrayArg stk doExport++    where marshalArrayArg stk doExport =+            allocaArray (fromInteger (product sizes)) \ptr -> do+              -- Traverse the nested sequences and write the elements to the+              -- array in order.+              -- ns is the dimensions of the values we are currently+              -- processing.+              -- vs is the values we are currently processing.+              -- nvss is the stack of previous ns and vs that we keep track of+              -- that we push onto when we start processing a nested sequence+              -- and pop off when we finish processing the current ones.+              -- i is the index into the array.++              let+                  -- write next element of multi-dimensional array+                  write (n:ns) (v:vs) nvss !i =+                    do vs' <- traverse (runEval stk)+                                       (enumerateSeqMap n (fromVSeq v))+                       write ns vs' ((n, vs):nvss) i++                  -- write next element in flat array+                  write [] (v:vs) nvss !i =+                    doExport v \rep ->+                      do pokeElemOff ptr i rep+                         write [] vs nvss (i + 1)++                  -- finished with flat array, do next element of multi-d array+                  write ns [] ((n, vs):nvss) !i = write (n:ns) vs nvss i++                  -- done+                  write _ _ [] _ = pure ()+++              write sizes [val] [] 0+              runEval stk $ f [SomeFFIArg ptr]++  marshalArg (FFITuple types) val f =+    do vals <- sequence (fromVTuple val)+       marshalArgs (types `zip` vals) f++  marshalArg (FFIRecord typeMap) val f =+    do vals <- traverse (`lookupRecord` val) (displayOrder typeMap)+       marshalArgs (displayElements typeMap `zip` vals) f++  -- Call marshalArg on a bunch of arguments and collect the results together+  -- (in the order of the arguments).+  marshalArgs ::+    [(FFIType, GenValue Concrete)] ->+    ([SomeFFIArg] -> Eval a) ->+    Eval a+  marshalArgs typesAndVals f = go typesAndVals []+    where+    go [] args = f (concat (reverse args))+    go ((t, v):tvs) prevArgs =+      marshalArg t v \currArgs ->+      go tvs (currArgs : prevArgs)++  -- Given an FFIType and a GetRet, obtain a return value and convert it to a+  -- Cryptol value. The return value is obtained differently depending on the+  -- FFIType.+  marshalRet :: FFIType -> GetRet -> Eval (GenValue Concrete)+  marshalRet FFIBool gr =+    do rep <- io (getRetAsValue gr @Word8)+       pure (VBit (toBool rep))++  marshalRet (FFIBasic (FFIBasicVal t)) gr =+    getMarshalBasicValRet t \doImport ->+      do rep <- io (getRetAsValue gr)+         doImport rep++  marshalRet (FFIBasic (FFIBasicRef t)) gr =+    getBasicRefRet t \how ->+    Eval             \stk ->+    alloca           \ptr ->+    bracket_ (initBasicRefRet how ptr) (clearBasicRefRet how ptr)+      do getRetAsOutArgs gr [SomeFFIArg ptr]+         rep <- peek ptr+         runEval stk (marshalBasicRefRet how rep)++  marshalRet (FFIArray (map evalFinType -> sizes) bt) gr =+    Eval \stk -> do+    let totalSize = fromInteger (product sizes)+        getResult marshal ptr = do+          getRetAsOutArgs gr [SomeFFIArg ptr]++          let build (n:ns) !i = do+                -- We need to be careful to actually run this here and not just+                -- stick the IO action into the sequence with io, or else we+                -- will read from the array after it is deallocated.+                vs <- for [0 .. fromInteger n - 1] \j ->+                  build ns (i * fromInteger n + j)+                pure (VSeq n (finiteSeqMap Concrete (map pure vs)))+              build [] !i = peekElemOff ptr i >>= runEval stk . marshal++          build sizes 0++    case bt of++      FFIBasicVal t ->+        getMarshalBasicValRet t \doImport ->+        allocaArray totalSize (getResult doImport)++      FFIBasicRef t ->+        getBasicRefRet t      \how ->+        allocaArray totalSize \ptr ->+          do let forEach f = for_ [0 .. totalSize - 1] (f . advancePtr ptr)+             bracket_ (forEach (initBasicRefRet how))+                      (forEach (clearBasicRefRet how))+                      (getResult (marshalBasicRefRet how) ptr)++  marshalRet (FFITuple types) gr = VTuple <$> marshalMultiRet types gr++  marshalRet (FFIRecord typeMap) gr =+    VRecord . recordFromFields . zip (displayOrder typeMap) <$>+      marshalMultiRet (displayElements typeMap) gr++  -- Obtain multiple return values as output arguments for a composite return+  -- type. Each return value is fully evaluated but put back in an Eval since+  -- VTuple and VRecord expect it.+  marshalMultiRet :: [FFIType] -> GetRet -> Eval [Eval (GenValue Concrete)]+  -- Since IO callbacks are involved we just do the whole thing in IO and wrap+  -- it in an Eval at the end. This should be fine since we are not changing+  -- the (Cryptol) call stack.+  marshalMultiRet types gr = Eval \stk -> do+    -- We use this IORef hack here since we are calling marshalRet recursively+    -- but marshalRet doesn't let us return any extra information from the+    -- callback through to the result of the function. So we remember the result+    -- as a side effect.+    vals <- newIORef []+    let go [] args = getRetAsOutArgs gr args+        go (t:ts) prevArgs = do+          val <- runEval stk $ marshalRet t $ getRetFromAsOutArgs \currArgs ->+            go ts (prevArgs ++ currArgs)+          modifyIORef' vals (val :)+    go types []+    map pure <$> readIORef vals++  -- | Call the callback with a 'BasicRefRet' for the given type.+  getBasicRefRet :: FFIBasicRefType ->+    (forall a. Storable a => BasicRefRet a -> b) -> b+  getBasicRefRet (FFIInteger mbMod) f = f BasicRefRet+    { initBasicRefRet = mpz_init+    , clearBasicRefRet = mpz_clear+    , marshalBasicRefRet = \mpz -> do+        n <- io $ peekInteger' mpz+        VInteger <$>+          case mbMod of+            Nothing -> pure n+            Just m  -> intToZn Concrete (evalFinType m) n }+  getBasicRefRet FFIRational f = f BasicRefRet+    { initBasicRefRet = mpq_init+    , clearBasicRefRet = mpq_clear+    , marshalBasicRefRet = \mpq -> do+        r <- io $ peekRational' mpq+        pure $ VRational $ SRational (numerator r) (denominator r) }++  -- Evaluate a finite numeric type expression.+  evalFinType :: Type -> Integer+  evalFinType = finNat' . evalNumType tenv++-- | Given a way to 'getRetAsOutArgs', create a 'GetRet', where the+-- 'getRetAsValue' simply allocates a temporary space to call 'getRetAsOutArgs'+-- on. This is useful for return types that we know how to obtain directly as a+-- value but need to obtain as an output argument when multiple return values+-- are involved.+getRetFromAsOutArgs :: ([SomeFFIArg] -> IO ()) -> GetRet+getRetFromAsOutArgs f = GetRet+  { getRetAsValue = alloca \ptr -> do+      f [SomeFFIArg ptr]+      peek ptr+  , getRetAsOutArgs = f }++-- | Given a 'FFIBasicValType', call the callback with a marshalling function+-- that marshals values to the 'FFIArg' type corresponding to the+-- 'FFIBasicValType'. The callback must be able to handle marshalling functions+-- that marshal to any 'FFIArg' type.+getMarshalBasicValArg ::+  FFIBasicValType ->+  (forall rep.+      FFIArg rep =>+      (GenValue Concrete -> Eval rep) ->+      result) ->+  result++getMarshalBasicValArg (FFIWord _ s) f = withWordType s \(_ :: p t) ->+  f @t $ fmap (fromInteger . bvVal) . fromVWord Concrete "getMarshalBasicValArg"++getMarshalBasicValArg (FFIFloat _ _ s) f =+  case s of+    -- LibBF can only convert to 'Double' directly, so we do that first then+    -- convert to 'Float', which should not result in any loss of precision if+    -- the original data was 32-bit anyways.+    FFIFloat32 -> f $ pure . CFloat . double2Float . toDouble+    FFIFloat64 -> f $ pure . CDouble . toDouble+  where+  toDouble = fst . bfToDouble NearEven . bfValue . fromVFloat++-- | Given a 'FFIBasicValType', call the callback with an unmarshalling function+-- from the 'FFIRet' type corresponding to the 'FFIBasicValType' to Cryptol+-- values. The callback must be able to handle unmarshalling functions from any+-- 'FFIRet' type.+getMarshalBasicValRet :: FFIBasicValType ->+  (forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b) -> b+getMarshalBasicValRet (FFIWord n s) f = withWordType s \(_ :: p t) ->+  f @t $ word Concrete n . toInteger+getMarshalBasicValRet (FFIFloat e p s) f =+  case s of+    FFIFloat32 -> f $ toValue . \case CFloat x -> float2Double x+    FFIFloat64 -> f $ toValue . \case CDouble x -> x+  where toValue = pure . VFloat . BF e p . bfFromDouble++-- | Call the callback with the Word type corresponding to the given+-- 'FFIWordSize'.+withWordType :: FFIWordSize ->+  (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b) -> b+withWordType FFIWord8  f = f $ Proxy @Word8+withWordType FFIWord16 f = f $ Proxy @Word16+withWordType FFIWord32 f = f $ Proxy @Word32+withWordType FFIWord64 f = f $ Proxy @Word64++-- | Given a 'FFIBasicRefType', call the callback with a marshalling function+-- that takes a Cryptol value and calls its callback with the 'Storable' type+-- corresponding to the 'FFIBasicRefType'.+getMarshalBasicRefArg :: FFIBasicRefType ->+  (forall rep.+      Storable rep =>+      (GenValue Concrete -> (rep -> IO val) -> IO val) ->+      result) ->+  result+getMarshalBasicRefArg (FFIInteger _) f = f \val g ->+  withInInteger' (fromVInteger val) g+getMarshalBasicRefArg FFIRational f = f \val g -> do+  let SRational {..} = fromVRational val+  withInRational' (sNum % sDenom) g++#else++-- | Dummy implementation for when FFI is disabled. Does not add anything to+-- the environment.+evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->+  Eval (Either [FFILoadError] EvalEnv)+evalForeignDecls _ _ env = pure $ Right env++#endif

@@ -0,0 +1,196 @@+{-# LANGUAGE BlockArguments   #-}+{-# LANGUAGE LambdaCase       #-}+{-# LANGUAGE RecordWildCards  #-}+{-# LANGUAGE TypeApplications #-}++-- | Generate C header files from foreign declarations.+module Cryptol.Eval.FFI.GenHeader+  ( generateForeignHeader+  ) where++import           Control.Monad.Writer.Strict+import           Data.Functor+import           Data.Char(isAlphaNum)+import           Data.List+import           Data.Set                      (Set)+import qualified Data.Set                      as Set+import           Language.C99.Pretty           as C+import qualified Language.C99.Simple           as C+import qualified Text.PrettyPrint              as Pretty++import           Cryptol.ModuleSystem.Name+import           Cryptol.TypeCheck.FFI.FFIType+import           Cryptol.TypeCheck.Type+import           Cryptol.Utils.Ident+import           Cryptol.Utils.RecordMap++-- | @Include foo@ represents an include statement @#include <foo>@+newtype Include = Include String deriving (Eq, Ord)++-- | The monad for generating headers. We keep track of which headers we need to+-- include and add them to the output at the end.+type GenHeaderM = Writer (Set Include)++-- | Generate a C header file from the given foreign declarations.+generateForeignHeader :: [(Name, FFIFunType)] -> String+generateForeignHeader decls =+  unlines (map renderInclude $ Set.toAscList incs)+  ++ Pretty.render (C.pretty $ C.translate (C.TransUnit cdecls []))+  where (cdecls, incs) = runWriter $ traverse convertFun decls++renderInclude :: Include -> String+renderInclude (Include inc) = "#include <" ++ inc ++ ">"++-- | The "direction" of a parameter (input or output).+data ParamDir = In | Out++-- | The result of converting a Cryptol type into its C representation.+data ConvertResult+  = Direct C.Type -- ^ A type that can be directly returned if it is a return+                  -- type and passed as a single parameter if it is a Cryptol+                  -- parameter type.+  | Params [C.Param] -- ^ A type that is turned into a number of parameters,+                     -- for both Cryptol parameter and return type cases.++-- | Convert a Cryptol foreign declaration into a C function declaration.+convertFun :: (Name, FFIFunType) -> GenHeaderM C.Decln+convertFun (fName, FFIFunType {..}) = do+  let tpIdent = fmap nameIdent . tpName+  typeParams <- traverse convertTypeParam (pickNames (map tpIdent ffiTParams))+  -- Name the input args in0, in1, etc+  let inPrefixes =+        case ffiArgTypes of+          [_] -> ["in"]+          _   -> ["in" ++ show @Integer i | i <- [0..]]+  inParams <- convertMultiType In $ zip inPrefixes ffiArgTypes+  (retType, outParams) <- convertType Out ffiRetType+    <&> \case+      Direct u  -> (u, [])+      -- Name the output arg out+      Params ps -> (C.TypeSpec C.Void, map (prefixParam "out") ps)+  -- Avoid possible name collisions+  let params = snd $ mapAccumL renameParam Set.empty $+        typeParams ++ inParams ++ outParams+      renameParam names (C.Param u name) =+        (Set.insert name' names, C.Param u name')+        where name' = until (`Set.notMember` names) (++ "_") name+  pure $ C.FunDecln Nothing retType (unpackIdent $ nameIdent fName) params+++-- | Convert a Cryptol type parameter to a C value parameter.+convertTypeParam :: String -> GenHeaderM C.Param+convertTypeParam name = (`C.Param` name) <$> sizeT++-- | Convert a Cryptol parameter or return type to C.+convertType :: ParamDir -> FFIType -> GenHeaderM ConvertResult+convertType _ FFIBool = Direct <$> uint8T+convertType _ (FFIBasic t) = convertBasicType t+convertType _ (FFIArray _ t) = do+  u <- convertBasicTypeInArray t+  pure $ Params [C.Param (C.Ptr u) ""]+convertType dir (FFITuple ts) = Params <$> convertMultiType dir+  -- We name the tuple components using their indices+  (zip (map (componentSuffix . show @Integer) [0..]) ts)+convertType dir (FFIRecord tMap) =+  Params <$> convertMultiType dir (zip names ts)+  where+  (fs,ts) = unzip (displayFields tMap)+  names   = map componentSuffix (pickNames (map Just fs))++-- | Convert many Cryptol types, each associated with a prefix, to C parameters+-- named with their prefixes.+convertMultiType :: ParamDir -> [(C.Ident, FFIType)] -> GenHeaderM [C.Param]+convertMultiType dir = fmap concat . traverse \(prefix, t) ->+  convertType dir t+    <&> \case+      Direct u -> [C.Param u' prefix]+        where u' = case dir of+                In  -> u+                -- Turn direct return types into pointer out parameters+                Out -> C.Ptr u+      Params ps -> map (prefixParam prefix) ps++{- | Convert a basic Cryptol FFI type to a C type with its corresponding+calling convention.  At present all value types use the same calling+convention no matter if they are inputs or outputs, so we don't+need the 'ParamDir'. -}+convertBasicType :: FFIBasicType -> GenHeaderM ConvertResult+convertBasicType bt =+  case bt of+    FFIBasicVal bvt -> Direct <$> convertBasicValType bvt+    FFIBasicRef brt -> do t <- convertBasicRefType brt+                          pure (Params [C.Param t ""])++-- | Convert a basic Cryptol FFI type to a C type.+-- This is used when the type is stored in array.+convertBasicTypeInArray :: FFIBasicType -> GenHeaderM C.Type+convertBasicTypeInArray bt =+  case bt of+    FFIBasicVal bvt -> convertBasicValType bvt+    FFIBasicRef brt -> convertBasicRefType brt++-- | Convert a basic Cryptol FFI type to a value C type.+convertBasicValType :: FFIBasicValType -> GenHeaderM C.Type+convertBasicValType (FFIWord _ s) =+  case s of+    FFIWord8  -> uint8T+    FFIWord16 -> uint16T+    FFIWord32 -> uint32T+    FFIWord64 -> uint64T+convertBasicValType (FFIFloat _ _ s) =+  case s of+    FFIFloat32 -> pure $ C.TypeSpec C.Float+    FFIFloat64 -> pure $ C.TypeSpec C.Double++-- | Convert a basic Cryptol FFI type to a reference C type.+convertBasicRefType :: FFIBasicRefType -> GenHeaderM C.Type+convertBasicRefType brt =+  case brt of+    FFIInteger {} -> mpzT+    FFIRational   -> mpqT++prefixParam :: C.Ident -> C.Param -> C.Param+prefixParam pre (C.Param u name) = C.Param u (pre ++ name)++-- | Create a suffix corresponding to some component name of some larger type.+componentSuffix :: String -> C.Ident+componentSuffix = ('_' :)++sizeT, uint8T, uint16T, uint32T, uint64T, mpzT, mpqT :: GenHeaderM C.Type+sizeT = typedefFromInclude stddefH "size_t"+uint8T = typedefFromInclude stdintH "uint8_t"+uint16T = typedefFromInclude stdintH "uint16_t"+uint32T = typedefFromInclude stdintH "uint32_t"+uint64T = typedefFromInclude stdintH "uint64_t"+mpzT = typedefFromInclude gmpH "mpz_t"+mpqT = typedefFromInclude gmpH "mpq_t"++stddefH, stdintH, gmpH :: Include+stddefH = Include "stddef.h"+stdintH = Include "stdint.h"+gmpH = Include "gmp.h"+++-- | Return a type with the given name, included from some header file.+typedefFromInclude :: Include -> C.Ident -> GenHeaderM C.Type+typedefFromInclude inc u = do+  tell $ Set.singleton inc+  pure $ C.TypeSpec $ C.TypedefName u++-- | Given some Cryptol identifiers (normal ones, not operators)+-- pick suitable unique C names for them+pickNames :: [Maybe Ident] -> [String]+pickNames xs = snd (mapAccumL add Set.empty xs)+  where+  add known x =+    let y      = simplify x+        ys     = y : [ y ++ show i | i <- [ 0 :: Int .. ] ]+        y' : _ = dropWhile (`Set.member` known) ys+    in (Set.insert y' known, y')++  simplify x = case x of+                 Just i | let y = filter ok (unpackIdent i), not (null y) -> y+                 _ -> "zz"++  ok x     = x == '_' || isAlphaNum x+

@@ -1452,12 +1452,12 @@   PNumPoly \first ->   PNumPoly \lst ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty in     case (first, lst) of       (Nat first', Nat lst') ->         let len = 1 + (lst' - first')-        in VSeq len $ indexSeqMap $ \i -> f (first' + i)+        in mkSeq sym (Nat len) ty $ indexSeqMap $ \i -> f (first' + i)       _ -> evalPanic "fromToV" ["invalid arguments"]  {-# INLINE fromThenToV #-}@@ -1469,12 +1469,12 @@   PNumPoly \lst   ->   PTyPoly  \ty    ->   PNumPoly \len   ->-  PVal+  PPrim     let !f = mkLit sym ty in     case (first, next, lst, len) of       (Nat first', Nat next', Nat _lst', Nat len') ->         let diff = next' - first'-        in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff)+        in mkSeq sym (Nat len') ty $ indexSeqMap $ \i -> f (first' + i*diff)       _ -> evalPanic "fromThenToV" ["invalid arguments"]  {-# INLINE fromToLessThanV #-}@@ -1484,12 +1484,12 @@   PFinPoly \first ->   PNumPoly \bound ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty         ss = indexSeqMap $ \i -> f (first + i)     in case bound of-         Inf        -> VStream ss-         Nat bound' -> VSeq (bound' - first) ss+         Inf        -> return $ VStream ss+         Nat bound' -> mkSeq sym (Nat (bound' - first)) ty ss  {-# INLINE fromToByV #-} -- @[ 0 .. 10 by 2 ]@@@ -1499,10 +1499,10 @@   PFinPoly \lst ->   PFinPoly \stride ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty         ss = indexSeqMap $ \i -> f (first + i*stride)-     in VSeq (1 + ((lst - first) `div` stride)) ss+     in mkSeq sym (Nat (1 + ((lst - first) `div` stride))) ty ss  {-# INLINE fromToByLessThanV #-} -- @[ 0 .. <10 by 2 ]@@@ -1512,12 +1512,12 @@   PNumPoly \bound ->   PFinPoly \stride ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty         ss = indexSeqMap $ \i -> f (first + i*stride)      in case bound of-          Inf -> VStream ss-          Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss+          Inf -> return $ VStream ss+          Nat bound' -> mkSeq sym (Nat ((bound' - first + stride - 1) `div` stride)) ty ss   {-# INLINE fromToDownByV #-}@@ -1528,10 +1528,10 @@   PFinPoly \lst ->   PFinPoly \stride ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty         ss = indexSeqMap $ \i -> f (first - i*stride)-     in VSeq (1 + ((first - lst) `div` stride)) ss+     in mkSeq sym (Nat (1 + ((first - lst) `div` stride))) ty ss  {-# INLINE fromToDownByGreaterThanV #-} -- @[ 10 .. >0 down by 2 ]@@@ -1541,10 +1541,10 @@   PFinPoly \bound ->   PFinPoly \stride ->   PTyPoly  \ty ->-  PVal+  PPrim     let !f = mkLit sym ty         ss = indexSeqMap $ \i -> f (first - i*stride)-     in VSeq ((first - bound + stride - 1) `div` stride) ss+     in mkSeq sym (Nat ((first - bound + stride - 1) `div` stride)) ty ss  {-# INLINE infFromV #-} infFromV :: Backend sym => sym -> Prim sym

@@ -10,6 +10,8 @@ > {-# LANGUAGE BlockArguments #-} > {-# LANGUAGE PatternGuards #-} > {-# LANGUAGE LambdaCase #-}+> {-# LANGUAGE NamedFieldPuns #-}+> {-# LANGUAGE ViewPatterns #-} > > module Cryptol.Eval.Reference >   ( Value(..)@@ -32,6 +34,7 @@ > import LibBF (BigFloat) > import qualified LibBF as FP > import qualified GHC.Num.Compat as Integer+> import qualified Data.List as List > > import Cryptol.ModuleSystem.Name (asPrim) > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)@@ -46,6 +49,8 @@ > import Cryptol.Utils.Panic (panic) > import Cryptol.Utils.PP > import Cryptol.Utils.RecordMap+> import Cryptol.Eval (checkProp)+> import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy) > > import qualified Cryptol.ModuleSystem as M > import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)@@ -332,12 +337,28 @@ >     EProofAbs _ e  -> evalExpr env e >     EProofApp e    -> evalExpr env e >     EWhere e dgs   -> evalExpr (foldl evalDeclGroup env dgs) e-+>+>     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"]  > 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 +> -- according to `envTypes` and expanding all type synonyms via `tNoUser`.+> evalProp :: Env -> Prop -> Prop+> evalProp env@Env { envTypes } = \case+>   TCon tc tys -> TCon tc (toType . evalType envTypes <$> tys)+>   TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty+>   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 +>     toType = either tNumTy tValTy + Selectors --------- @@ -510,8 +531,9 @@ > evalDecl :: Env -> Decl -> (Name, E Value) > evalDecl env d = >   case dDefinition d of->     DPrim   -> (dName d, pure (evalPrim (dName d)))->     DExpr e -> (dName d, evalExpr env e)+>     DPrim      -> (dName d, pure (evalPrim (dName d)))+>     DForeign _ -> (dName d, cryError $ FFINotSupported $ dName d)+>     DExpr e    -> (dName d, evalExpr env e) >  Newtypes@@ -523,7 +545,7 @@ that consumes and ignores its type arguments.  > evalNewtypeDecl :: Env -> Newtype -> Env-> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env+> evalNewtypeDecl env nt = bindVar (ntConName nt, pure val) env >   where >     val = foldr tabs con (ntParams nt) >     con = VFun (\x -> x)

@@ -8,6 +8,7 @@  {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-}

@@ -18,6 +18,7 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.RecordMap+import Cryptol.Utils.Types  import Data.Maybe(fromMaybe) import qualified Data.IntMap.Strict as IntMap@@ -27,7 +28,7 @@ -- | An evaluated type of kind *. -- These types do not contain type variables, type synonyms, or type functions. data TValue-  = TVBit                     -- ^ @ Bit @+  = TVBit                     -- ^ @ Bit @     | TVInteger                 -- ^ @ Integer @   | TVFloat Integer Integer   -- ^ @ Float e p @   | TVIntMod Integer          -- ^ @ Z n @@@ -86,6 +87,10 @@ tvSeq (Nat n) t = TVSeq n t tvSeq Inf     t = TVStream t +-- | The Cryptol @Float64@ type.+tvFloat64 :: TValue+tvFloat64 = uncurry TVFloat float64ExpPrec+ -- | Coerce an extended natural into an integer, --   for values known to be finite finNat' :: Nat' -> Integer@@ -100,6 +105,7 @@ newtype TypeEnv =   TypeEnv   { envTypeMap  :: IntMap.IntMap (Either Nat' TValue) }+  deriving (Show)  instance Monoid TypeEnv where   mempty = TypeEnv mempty

@@ -6,6 +6,7 @@  {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiWayIf #-}@@ -505,7 +506,7 @@   TValue ->   SInteger (What4 sym) ->   SEval (What4 sym) (Value sym)-indexFront_int sym mblen _a xs ix idx+indexFront_int sym mblen _a xs _ix idx   | Just i <- W4.asInteger idx   = lookupSeqMap xs i @@ -535,16 +536,13 @@           _                        -> Nothing       ) -    -- Maximum possible in-bounds index given `Z m`-    -- type information and the length-    -- of the sequence. If the sequences is infinite and the-    -- integer is unbounded, there isn't much we can do.+    -- Maximum possible in-bounds index given the length+    -- of the sequence. If the sequence is infinite, there+    -- isn't much we can do.     maxIdx =-      case (mblen, ix) of-        (Nat n, TVIntMod m)  -> Just (min (toInteger n) (toInteger m))-        (Nat n, _)           -> Just n-        (_    , TVIntMod m)  -> Just m-        _                    -> Nothing+      case mblen of+        Nat n -> Just (n - 1)+        Inf   -> Nothing indexFront_segs ::   W4.IsSymExprBuilder sym =>   What4 sym ->

@@ -93,6 +93,7 @@ instance FreeVars DeclDef where   freeVars d = case d of                  DPrim -> mempty+                 DForeign _ -> mempty                  DExpr e -> freeVars e  @@ -116,6 +117,7 @@       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 ]     where       foldFree :: (FreeVars a, Defs a) => [a] -> Deps       foldFree = foldr updateFree mempty

@@ -0,0 +1,267 @@+{-# Language ImplicitParams #-}+module Cryptol.IR.TraverseNames where++import Data.Set(Set)+import qualified Data.Set as Set+import Data.Functor.Identity++import Cryptol.ModuleSystem.Name(nameUnique)+import Cryptol.Utils.RecordMap(traverseRecordMap)+import Cryptol.Parser.Position(Located(..))+import Cryptol.TypeCheck.AST+import Cryptol.TypeCheck.FFI.FFIType++traverseNames ::+  (TraverseNames t, Applicative f) => (Name -> f Name) -> (t -> f t)+traverseNames f = let ?name = f in traverseNamesIP++mapNames :: (TraverseNames t) => (Name -> Name) -> t -> t+mapNames f x = result+  where+  Identity result = let ?name = pure . f+                    in traverseNamesIP x++class TraverseNames t where+  traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => t -> f t++instance TraverseNames a => TraverseNames [a] where+  traverseNamesIP = traverse traverseNamesIP++instance TraverseNames a => TraverseNames (Maybe a) where+  traverseNamesIP = traverse traverseNamesIP++instance (Ord a, TraverseNames a) => TraverseNames (Set a) where+  traverseNamesIP = fmap Set.fromList . traverseNamesIP . Set.toList++instance TraverseNames a => TraverseNames (Located a) where+  traverseNamesIP (Located r a) = Located r <$> traverseNamesIP a++instance TraverseNames Name where+  traverseNamesIP = ?name++instance (Ord a, TraverseNames a) => TraverseNames (ExportSpec a) where+  traverseNamesIP (ExportSpec mp) = ExportSpec <$> traverse traverseNamesIP mp++instance TraverseNames Expr where+  traverseNamesIP expr =+    case expr of+      EList es t        -> EList  <$> traverseNamesIP es <*> traverseNamesIP t++      ETuple es         -> ETuple <$> traverseNamesIP es++      ERec mp           -> ERec <$> traverseRecordMap (\_ -> traverseNamesIP) mp++      ESel e l          -> (`ESel` l) <$> traverseNamesIP e++      ESet t e1 l e2    -> ESet <$> traverseNamesIP t+                                <*> traverseNamesIP e1+                                <*> pure l+                                <*> traverseNamesIP e2++      EIf e1 e2 e3      -> EIf <$> traverseNamesIP e1+                               <*> traverseNamesIP e2+                               <*> traverseNamesIP e3++      EComp t1 t2 e mss -> EComp <$> traverseNamesIP t1+                                 <*> traverseNamesIP t2+                                 <*> traverseNamesIP e+                                 <*> traverseNamesIP mss++      EVar x            -> EVar <$> traverseNamesIP x+      ETAbs tp e        -> ETAbs <$> traverseNamesIP tp <*> traverseNamesIP e+      ETApp e t         -> ETApp <$> traverseNamesIP e <*> traverseNamesIP t+      EApp e1 e2        -> EApp <$> traverseNamesIP e1 <*> traverseNamesIP e2+      EAbs x t e        -> EAbs <$> traverseNamesIP x+                                <*> traverseNamesIP t+                                <*> traverseNamesIP e+      ELocated r e      -> ELocated r <$> traverseNamesIP e+      EProofAbs p e     -> EProofAbs <$> traverseNamesIP p <*> traverseNamesIP e+      EProofApp e       -> EProofApp <$> traverseNamesIP e+      EWhere e ds       -> EWhere <$> traverseNamesIP e <*> traverseNamesIP ds++      EPropGuards gs t  -> EPropGuards <$> traverse doG gs <*> traverseNamesIP t+        where doG (xs, e) = (,) <$> traverseNamesIP xs <*> traverseNamesIP e++instance TraverseNames Match where+  traverseNamesIP mat =+    case mat of+      From x t1 t2 e -> From <$> traverseNamesIP x+                             <*> traverseNamesIP t1+                             <*> traverseNamesIP t2+                             <*> traverseNamesIP e+      Let d          -> Let <$> traverseNamesIP d++instance TraverseNames DeclGroup where+  traverseNamesIP dg =+    case dg of+      NonRecursive d -> NonRecursive <$> traverseNamesIP d+      Recursive ds   -> Recursive    <$> traverseNamesIP ds++instance TraverseNames Decl where+  traverseNamesIP decl = mk <$> traverseNamesIP (dName decl)+                            <*> traverseNamesIP (dSignature decl)+                            <*> traverseNamesIP (dDefinition decl)+    where mk nm sig def = decl { dName = nm+                               , dSignature = sig+                               , dDefinition = def+                               }++instance TraverseNames DeclDef where+  traverseNamesIP d =+    case d of+      DPrim   -> pure d+      DForeign t -> DForeign <$> traverseNamesIP t+      DExpr e -> DExpr <$> traverseNamesIP e++instance TraverseNames Schema where+  traverseNamesIP (Forall as ps t) =+    Forall <$> traverseNamesIP as+           <*> traverseNamesIP ps+           <*> traverseNamesIP t++instance TraverseNames TParam where+  traverseNamesIP tp = mk <$> traverseNamesIP (tpFlav tp)+                          <*> traverseNamesIP (tpInfo tp)+    -- XXX: module parameters should probably be represented directly+    -- as (abstract) user-defined types, rather than type variables.+    where mk f i = case f of+                     TPModParam x ->+                      tp { tpUnique = nameUnique x, tpFlav = f, tpInfo = i }+                     _ -> tp { tpFlav = f, tpInfo = i }+++instance TraverseNames TPFlavor where+  traverseNamesIP tpf =+    case tpf of+      TPModParam x      -> TPModParam     <$> traverseNamesIP x+      TPUnifyVar        -> pure tpf+      TPSchemaParam x   -> TPSchemaParam  <$> traverseNamesIP x+      TPTySynParam x    -> TPTySynParam   <$> traverseNamesIP x+      TPPropSynParam x  -> TPPropSynParam <$> traverseNamesIP x+      TPNewtypeParam x  -> TPNewtypeParam <$> traverseNamesIP x+      TPPrimParam x     -> TPPrimParam    <$> traverseNamesIP x++instance TraverseNames TVarInfo where+  traverseNamesIP (TVarInfo r s) = TVarInfo r <$> traverseNamesIP s++instance TraverseNames TypeSource where+  traverseNamesIP src =+    case src of+      TVFromModParam x            -> TVFromModParam <$> traverseNamesIP x+      TVFromSignature x           -> TVFromSignature <$> traverseNamesIP x+      TypeWildCard                -> pure src+      TypeOfRecordField {}        -> pure src+      TypeOfTupleField {}         -> pure src+      TypeOfSeqElement            -> pure src+      LenOfSeq                    -> pure src+      TypeParamInstNamed x i      -> TypeParamInstNamed <$> traverseNamesIP x+                                                        <*> pure i+      TypeParamInstPos   x i      -> TypeParamInstPos   <$> traverseNamesIP x+                                                        <*> pure i+      DefinitionOf x              -> DefinitionOf <$> traverseNamesIP x+      LenOfCompGen                -> pure src+      TypeOfArg arg               -> TypeOfArg <$> traverseNamesIP arg+      TypeOfRes                   -> pure src+      FunApp                      -> pure src+      TypeOfIfCondExpr            -> pure src+      TypeFromUserAnnotation      -> pure src+      GeneratorOfListComp         -> pure src+      TypeErrorPlaceHolder        -> pure src++instance TraverseNames ArgDescr where+  traverseNamesIP arg = mk <$> traverseNamesIP (argDescrFun arg)+    where mk n = arg { argDescrFun = n }++instance TraverseNames Type where+  traverseNamesIP ty =+    case ty of+      TCon tc ts    -> TCon <$> traverseNamesIP 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+++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 ModTParam where+  traverseNamesIP nt = mk <$> traverseNamesIP (mtpName nt)+    where+    mk x = nt { mtpName = x }++instance TraverseNames ModVParam where+  traverseNamesIP nt = mk <$> traverseNamesIP (mvpName nt)+                          <*> traverseNamesIP (mvpType nt)+    where+    mk x t = nt { mvpName = x, mvpType = t }++instance TraverseNames FFIFunType where+  traverseNamesIP fi = mk <$> traverseNamesIP (ffiArgTypes fi)+                          <*> traverseNamesIP (ffiRetType fi)+    where+    mk as b =+      FFIFunType+        { ffiTParams  = ffiTParams fi+        , ffiArgTypes = as+        , ffiRetType  = b+        }++instance TraverseNames FFIType where+  traverseNamesIP ft =+    case ft of+      FFIBool       -> pure ft+      FFIBasic _    -> pure ft   -- assumes no names here+      FFIArray sz t -> (`FFIArray` t) <$> traverseNamesIP sz+      FFITuple ts   -> FFITuple  <$> traverseNamesIP ts+      FFIRecord mp  -> FFIRecord <$> traverseRecordMap+                                                (\_ -> traverseNamesIP) mp+instance TraverseNames TySyn where+  traverseNamesIP ts = mk <$> traverseNamesIP (tsName ts)+                          <*> traverseNamesIP (tsParams ts)+                          <*> traverseNamesIP (tsConstraints ts)+                          <*> traverseNamesIP (tsDef ts)+    where mk n ps cs t =+            TySyn  { tsName        = n+                   , tsParams      = ps+                   , tsConstraints = cs+                   , tsDef         = t+                   , tsDoc         = tsDoc ts+                   }++

@@ -7,6 +7,7 @@ -- Portability :  portable  {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE BlockArguments #-}  module Cryptol.ModuleSystem (     -- * Module System@@ -18,8 +19,10 @@   , findModule   , loadModuleByPath   , loadModuleByName+  , checkModuleByPath   , checkExpr   , evalExpr+  , benchmarkExpr   , checkDecls   , evalDecls   , noPat@@ -29,8 +32,11 @@   , renameType      -- * Interfaces-  , Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface-  , IfaceTySyn, IfaceDecl(..)+  , Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)++    -- * Dependencies+  , getFileDependencies+  , getModuleDependencies   ) where  import Data.Map (Map)@@ -47,6 +53,7 @@ import           Cryptol.Parser.NoPat (RemovePatterns) import qualified Cryptol.TypeCheck.AST     as T import qualified Cryptol.TypeCheck.Interface as T+import           Cryptol.Utils.Benchmark (BenchmarkStats) import qualified Cryptol.Utils.Ident as M  -- Public Interface ------------------------------------------------------------@@ -63,23 +70,34 @@ findModule n env = runModuleM env (Base.findModule n)  -- | Load the module contained in the given file.-loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)-loadModuleByPath path minp =-  runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do+loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.TCTopEntity)+loadModuleByPath path minp = do+  moduleEnv' <- resetModuleEnv $ minpModuleEnv minp+  runModuleM minp{ minpModuleEnv = moduleEnv' } $ do     unloadModule ((InFile path ==) . lmFilePath)-    m <- Base.loadModuleByPath path-    setFocusedModule (T.mName m)+    m <- Base.loadModuleByPath True path+    setFocusedModule (T.tcTopEntitytName m)     return (InFile path,m)  -- | Load the given parsed module.-loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)-loadModuleByName n minp =-  runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do+loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.TCTopEntity)+loadModuleByName n minp = do+  moduleEnv' <- resetModuleEnv $ minpModuleEnv minp+  runModuleM minp{ minpModuleEnv = moduleEnv' } $ do     unloadModule ((n ==) . lmName)     (path,m') <- Base.loadModuleFrom False (FromModule n)-    setFocusedModule (T.mName m')+    setFocusedModule (T.tcTopEntitytName m')     return (path,m') +-- | Parse and typecheck a module, but don't evaluate or change the environment.+checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, T.TCTopEntity)+checkModuleByPath path minp = do+  (res, warns) <- runModuleM minp $ Base.loadModuleByPath False path+  -- restore the old environment+  let res1 = do (x,_newEnv) <- res+                pure ((InFile path, x), minpModuleEnv minp)+  pure (res1, warns)+ -- Extended Environments -------------------------------------------------------  -- These functions are particularly useful for interactive modes, as@@ -95,6 +113,11 @@ evalExpr :: T.Expr -> ModuleCmd Concrete.Value evalExpr e env = runModuleM env (interactive (Base.evalExpr e)) +-- | Benchmark an expression.+benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats+benchmarkExpr period e env =+  runModuleM env (interactive (Base.benchmarkExpr period e))+ -- | Typecheck top-level declarations. checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn) checkDecls ds env = runModuleM env@@ -119,3 +142,16 @@ renameType :: R.NamingEnv -> PName -> ModuleCmd Name renameType names n env = runModuleM env $ interactive $   Base.rename M.interactiveName names (R.renameType R.NameUse n)++--------------------------------------------------------------------------------+-- Dependencies+++-- | Get information about the dependencies of a file.+getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo)+getFileDependencies f env = runModuleM env (Base.findDepsOf (InFile f))++-- | Get information about the dependencies of a module.+getModuleDependencies :: M.ModName -> ModuleCmd (ModulePath, FileInfo)+getModuleDependencies m env = runModuleM env (Base.findDepsOfModule m)+

@@ -11,17 +11,22 @@  {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE BlockArguments #-}  module Cryptol.ModuleSystem.Base where  import qualified Control.Exception as X-import Control.Monad (unless,when)+import Control.Monad (unless,forM)+import Data.Set(Set)+import qualified Data.Set as Set import Data.Maybe (fromMaybe)-import Data.Monoid ((<>))+import Data.List(sortBy,groupBy)+import Data.Function(on)+import Data.Monoid ((<>),Endo(..), Any(..)) import Data.Text.Encoding (decodeUtf8')-import Data.IORef(newIORef,readIORef) import System.Directory (doesFileExist, canonicalizePath) import System.FilePath ( addExtension                        , isAbsolute@@ -39,39 +44,45 @@   -import Cryptol.ModuleSystem.Env (DynamicEnv(..)) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Monad-import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..))-import Cryptol.ModuleSystem.Env (lookupModule-                                , LoadedModule(..)+import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..),nameIdent)+import Cryptol.ModuleSystem.Env ( DynamicEnv(..),FileInfo(..),fileInfo+                                , lookupModule+                                , lookupTCEntity+                                , LoadedModuleG(..), lmInterface                                 , meCoreLint, CoreLint(..)-                                , ModContext(..)+                                , ModContext(..), ModContextParams(..)                                 , ModulePath(..), modulePathLabel)+import           Cryptol.Backend.FFI import qualified Cryptol.Eval                 as E import qualified Cryptol.Eval.Concrete as Concrete import           Cryptol.Eval.Concrete (Concrete(..))+import           Cryptol.Eval.FFI import qualified Cryptol.ModuleSystem.NamingEnv as R import qualified Cryptol.ModuleSystem.Renamer as R import qualified Cryptol.Parser               as P import qualified Cryptol.Parser.Unlit         as P import Cryptol.Parser.AST as P import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))+import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards +  ( expandPropGuards, runExpandPropGuardsM ) import Cryptol.Parser.NoInclude (removeIncludesModule) import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange) import qualified Cryptol.TypeCheck     as T import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.PP as T import qualified Cryptol.TypeCheck.Sanity as TcSanity+import qualified Cryptol.Backend.FFI.Error as FFI -import Cryptol.Transform.AddModParams (addModParams) import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName                            , preludeReferenceName, interactiveName, modNameChunks-                           , notParamInstModName, isParamInstModName )+                           , modNameToNormalModName ) import Cryptol.Utils.PP (pretty) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint)+import Cryptol.Utils.Benchmark  import Cryptol.Prelude ( preludeContents, floatContents, arrayContents                        , suiteBContents, primeECContents, preludeReferenceContents )@@ -114,11 +125,22 @@   unless (null errs) (noPatErrors errs)   return a' +-- ExpandPropGuards ------------------------------------------------------------ +-- | Run the expandPropGuards pass.+expandPropGuards :: Module PName -> ModuleM (Module PName)+expandPropGuards a =+  case ExpandPropGuards.runExpandPropGuardsM $ ExpandPropGuards.expandPropGuards a of+    Left err -> expandPropGuardsError err+    Right a' -> pure a'+ -- Parsing ---------------------------------------------------------------------  -- | Parse a module and expand includes-parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)+-- Returns a fingerprint of the module, and a set of dependencies due+-- to `include` directives.+parseModule ::+  ModulePath -> ModuleM (Fingerprint, Set FilePath, [P.Module PName]) parseModule path = do   getBytes <- getByteReader @@ -150,111 +172,167 @@               }    case P.parseModule cfg txt of-    Right pm ->+    Right pms ->       do let fp = fingerprint bytes-         pm1 <- case path of-                  InFile p ->-                    do r <- getByteReader-                       mb <- io (removeIncludesModule r p pm)+         (pm1,deps) <-+           case path of+             InFile p ->+               do r <- getByteReader+                  (mo,d) <- unzip <$>+                    forM pms \pm ->+                    do mb <- io (removeIncludesModule r p pm)                        case mb of                          Right ok -> pure ok                          Left err -> noIncludeErrors err+                  pure (mo, Set.unions d) -                  {- We don't do "include" resolution for in-memory files-                     because at the moment the include resolution pass requires-                     the path to the file to be known---this is used when-                     looking for other inlcude files.  This could be-                     generalized, but we can do it once we have a concrete use-                     case as it would help guide the design. -}-                  InMem {} -> pure pm+             {- We don't do "include" resolution for in-memory files+                because at the moment the include resolution pass requires+                the path to the file to be known---this is used when+                looking for other inlcude files.  This could be+                generalized, but we can do it once we have a concrete use+                case as it would help guide the design. -}+             InMem {} -> pure (pms, Set.empty) -         fp `seq` return (fp, pm1)+{-+         case path of+           InFile {} -> io $ print (T.vcat (map T.pp pm1))+           InMem {} -> pure ()+--}+         fp `seq` return (fp, deps, pm1)      Left err -> moduleParseError path err  --- Modules ---------------------------------------------------------------------+-- Top Level Modules and Signatures -------------------------------------------- + -- | Load a module by its path.-loadModuleByPath :: FilePath -> ModuleM T.Module-loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do+loadModuleByPath ::+  Bool {- ^ evaluate declarations in the module -} ->+  FilePath -> ModuleM T.TCTopEntity+loadModuleByPath eval path = withPrependedSearchPath [ takeDirectory path ] $ do   let fileName = takeFileName path   foundPath <- findFile fileName-  (fp, pm) <- parseModule (InFile foundPath)-  let n = thing (P.mName pm)+  (fp, deps, pms) <- parseModule (InFile foundPath)+  last <$>+    forM pms \pm ->+    do let n = thing (P.mName pm) -  -- Check whether this module name has already been loaded from a different file-  env <- getModuleEnv-  -- path' is the resolved, absolute path, used only for checking-  -- whether it's already been loaded-  path' <- io (canonicalizePath foundPath)+       -- Check whether this module name has already been loaded from a+       -- different file+       env <- getModuleEnv+       -- path' is the resolved, absolute path, used only for checking+       -- whether it's already been loaded+       path' <- io (canonicalizePath foundPath) -  case lookupModule n env of-    -- loadModule will calculate the canonical path again-    Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm-    Just lm-     | path' == loaded -> return (lmModule lm)-     | otherwise       -> duplicateModuleName n path' loaded-     where loaded = lmModuleId lm+       case lookupTCEntity n env of+         -- loadModule will calculate the canonical path again+         Nothing ->+           doLoadModule eval False (FromModule n) (InFile foundPath) fp deps pm+         Just lm+          | path' == loaded -> return (lmData lm)+          | otherwise       -> duplicateModuleName n path' loaded+          where loaded = lmModuleId lm   -- | Load a module, unless it was previously loaded.-loadModuleFrom :: Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.Module)+loadModuleFrom ::+  Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.TCTopEntity) loadModuleFrom quiet isrc =   do let n = importedModule isrc      mb <- getLoadedMaybe n      case mb of-       Just m -> return (lmFilePath m, lmModule m)+       Just m -> return (lmFilePath m, lmData m)        Nothing ->          do path <- findModule n             errorInFile path $-              do (fp, pm) <- parseModule path-                 m        <- doLoadModule quiet isrc path fp pm-                 return (path,m)+              do (fp, deps, pms) <- parseModule path+                 ms <- mapM (doLoadModule True quiet isrc path fp deps) pms+                 return (path,last ms)  -- | Load dependencies, typecheck, and add to the eval environment. doLoadModule ::+  Bool {- ^ evaluate declarations in the module -} ->   Bool {- ^ quiet mode: true suppresses the "loading module" message -} ->   ImportSource ->   ModulePath ->   Fingerprint ->+  Set FilePath {- ^ `include` dependencies -} ->   P.Module PName ->-  ModuleM T.Module-doLoadModule quiet isrc path fp pm0 =+  ModuleM T.TCTopEntity+doLoadModule eval quiet isrc path fp incDeps pm0 =   loading isrc $   do let pm = addPrelude pm0-     loadDeps pm+     impDeps <- loadDeps pm +     let what = case P.mDef pm of+                  P.InterfaceModule {} -> "interface module"+                  _                    -> "module"+      unless quiet $ withLogger logPutStrLn-       ("Loading module " ++ pretty (P.thing (P.mName pm)))+       ("Loading " ++ what ++ " " ++ pretty (P.thing (P.mName pm)))  -     (nameEnv,tcmod) <- checkModule isrc pm-     tcm <- optionalInstantiate tcmod+     (nameEnv,tcm) <- checkModule isrc pm       -- extend the eval env, unless a functor.      tbl <- Concrete.primTable <$> getEvalOptsAction      let ?evalPrim = \i -> Right <$> Map.lookup i tbl      callStacks <- getCallStacks      let ?callStacks = callStacks-     unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)-     loadedModule path fp nameEnv tcm+     let shouldEval =+           case tcm of+             T.TCTopModule m | eval && not (T.isParametrizedModule m) -> Just m+             _ -> Nothing +     foreignSrc <- case shouldEval of+                      Just m ->+                        do fsrc <- evalForeign m+                           modifyEvalEnv (E.moduleEnv Concrete m)+                           pure fsrc+                      Nothing -> pure Nothing++     let fi = fileInfo fp incDeps impDeps foreignSrc+     loadedModule path fi nameEnv foreignSrc tcm+      return tcm+   where-  optionalInstantiate tcm-    | isParamInstModName (importedModule isrc) =-      if T.isParametrizedModule tcm then-        case addModParams tcm of-          Right tcm1 -> return tcm1-          Left xs    -> failedToParameterizeModDefs (T.mName tcm) xs-      else notAParameterizedModule (T.mName tcm)-    | otherwise = return tcm+  evalForeign tcm+    | not (null foreignFs) =+      ffiLoadErrors (T.mName tcm) (map FFI.FFIInFunctor foreignFs)+    | not (null dups) =+      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] +    where foreigns  = findForeignDecls tcm+          foreignFs = T.findForeignDeclsInFunctors tcm+          dups      = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)+                                           $ sortBy (compare `on` nameIdent)+                                           $ map fst foreigns ] + -- | Rewrite an import declaration to be of the form: -- -- > import foo as foo [ [hiding] (a,b,c) ]@@ -298,51 +376,149 @@ -- | Discover a file. This is distinct from 'findModule' in that we -- assume we've already been given a particular file name. findFile :: FilePath -> ModuleM FilePath-findFile path | isAbsolute path = do-  -- No search path checking for absolute paths-  b <- io (doesFileExist path)-  if b then return path else cantFindFile path-findFile path = do-  paths <- getSearchPath-  loop (possibleFiles paths)-  where-  loop paths = case paths of-    path':rest -> do-      b <- io (doesFileExist path')-      if b then return (normalise path') else loop rest-    [] -> cantFindFile path-  possibleFiles paths = map (</> path) paths+findFile path+  | isAbsolute path =+    do -- No search path checking for absolute paths+       b <- io (doesFileExist path)+       if b then return path else cantFindFile path+  | otherwise =+    do paths <- getSearchPath+       loop (possibleFiles paths)+       where+       loop paths = case paths of+                      path' : rest ->+                        do b <- io (doesFileExist path')+                           if b then return (normalise path') else loop rest+                      [] -> cantFindFile path+       possibleFiles paths = map (</> path) paths  -- | Add the prelude to the import list if it's not already mentioned. addPrelude :: P.Module PName -> P.Module PName addPrelude m   | preludeName == P.thing (P.mName m) = m   | preludeName `elem` importedMods    = m-  | otherwise                          = m { mDecls = importPrelude : mDecls m }+  | otherwise                          = m { mDef = newDef }   where+  newDef =+    case mDef m of+      NormalModule ds -> NormalModule (P.DImport prel : ds)+      FunctorInstance f as ins -> FunctorInstance f as ins+      InterfaceModule s -> InterfaceModule s { sigImports = prel+                                             : sigImports s }+   importedMods  = map (P.iModule . P.thing) (P.mImports m)-  importPrelude = P.DImport P.Located+  prel = P.Located     { P.srcRange = emptyRange     , P.thing    = P.Import-      { iModule    = P.ImpTop preludeName-      , iAs        = Nothing-      , iSpec      = Nothing+      { iModule  = P.ImpTop preludeName+      , iAs      = Nothing+      , iSpec    = Nothing+      , iInst    = Nothing       }     }  -- | Load the dependencies of a module into the environment.-loadDeps :: P.Module name -> ModuleM ()+loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName) loadDeps m =-  do mapM_ loadI (P.mImports m)-     mapM_ loadF (P.mInstance m)+  do let ds = findDeps m+     mapM_ (loadModuleFrom False) ds+     pure (Set.fromList (map importedModule ds))++-- | Find all imports in a module.+findDeps :: P.ModuleG mname name -> [ImportSource]+findDeps m = appEndo (snd (findDeps' m)) []++findDepsOfModule :: ModName -> ModuleM (ModulePath, FileInfo)+findDepsOfModule m =+  do mpath <- findModule m+     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+     let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms)+     fpath <- if getAny anyF+                then do mb <- io case mpath of+                                   InFile can -> foreignLibPath can+                                   InMem {}   -> pure Nothing+                        pure case mb of+                               Nothing -> Set.empty+                               Just f  -> Set.singleton f+                else pure Set.empty+     pure+       ( mpath+       , FileInfo+           { fiFingerprint = fp+           , fiIncludeDeps = incs+           , fiImportDeps  = Set.fromList (map importedModule (appEndo imps []))+           , fiForeignDeps = fpath+           }+       )++-- | Find the set of top-level modules imported by a module.+findModuleDeps :: P.ModuleG mname name -> Set P.ModName+findModuleDeps = Set.fromList . map importedModule . findDeps++-- | A helper `findDeps` and `findModuleDeps` that actually does the searching.+findDeps' :: P.ModuleG mname name -> (Any, Endo [ImportSource])+findDeps' m =+  case mDef m of+    NormalModule ds -> mconcat (map depsOfDecl ds)+    FunctorInstance f as _ ->+      let fds = loadImpName FromModuleInstance f+          ads = case as of+                  DefaultInstArg a -> loadInstArg a+                  DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds)+                  NamedInstArgs args -> mconcat (map loadNamedInstArg args)+      in fds <> ads+    InterfaceModule s -> mconcat (map loadImpD (sigImports s))   where-  loadI i = do (_,m1)  <- loadModuleFrom False (FromImport i)-               when (T.isParametrizedModule m1) $ importParamModule $ T.mName m1-  loadF f = do _ <- loadModuleFrom False (FromModuleInstance f)-               return ()+  loadI i = (mempty, Endo (i:)) +  loadImpName src l =+    case thing l of+      ImpTop f -> loadI (src l { thing = f })+      _        -> mempty +  loadImpD li = loadImpName (FromImport . new) (iModule <$> li)+    where new i = i { thing = (thing li) { iModule = thing i } } +  loadNamedInstArg (ModuleInstanceNamedArg _ f) = loadInstArg f+  loadInstArg f =+    case thing f of+      ModuleArg mo -> loadImpName FromModuleInstance f { thing = mo }+      _            -> mempty++  depsOfDecl d =+    case d of+      DImport li -> loadImpD li++      DModule TopLevel { tlValue = NestedModule nm } -> findDeps' nm++      DModParam mo -> loadImpName FromSigImport s+        where s = mpSignature mo++      Decl dd -> depsOfDecl' (tlValue dd)++      _ -> mempty++  depsOfDecl' d =+    case d of+      DLocated d' _ -> depsOfDecl' d'+      DBind b ->+        case thing (bDef b) of+          DForeign {} -> (Any True, mempty)+          _ -> mempty+      _ -> mempty++++++ -- Type Checking ---------------------------------------------------------------  -- | Typecheck a single expression, yielding a renamed parsed expression,@@ -405,46 +581,38 @@        Nothing -> panic "Cryptol.ModuleSystem.Base.getPrimMap"                   [ "Unable to find the prelude" ] --- | Load a module, be it a normal module or a functor instantiation.-checkModule :: ImportSource -> P.Module PName -> ModuleM (R.NamingEnv, T.Module)-checkModule isrc m =-  case P.mInstance m of-    Nothing -> checkSingleModule T.tcModule isrc m-    Just fmName ->-      do mbtf <- getLoadedMaybe (thing fmName)-         case mbtf of-           Just tf ->-             do renThis <- io $ newIORef (lmNamingEnv tf)-                let how = T.tcModuleInst renThis (lmModule tf)-                (_,m') <- checkSingleModule how isrc m-                newEnv <- io $ readIORef renThis-                pure (newEnv,m')-           Nothing -> panic "checkModule"-                        [ "Functor of module instantiation not loaded" ]----- | Typecheck a single module.  If the module is an instantiation--- of a functor, then this just type-checks the instantiating parameters.--- See 'checkModule'+-- | Typecheck a single module. -- Note: we assume that @include@s have already been processed-checkSingleModule ::-  Act (P.Module Name) T.Module {- ^ how to check -} ->-  ImportSource                 {- ^ why are we loading this -} ->-  P.Module PName               {- ^ module to check -} ->-  ModuleM (R.NamingEnv,T.Module)-checkSingleModule how isrc m = do+checkModule ::+  ImportSource                      {- ^ why are we loading this -} ->+  P.Module PName                    {- ^ module to check -} ->+  ModuleM (R.NamingEnv,T.TCTopEntity)+checkModule isrc m = do    -- check that the name of the module matches expectations   let nm = importedModule isrc-  unless (notParamInstModName nm == thing (P.mName m))+  unless (modNameToNormalModName nm ==+                                  modNameToNormalModName (thing (P.mName m)))          (moduleNameMismatch nm (mName m))    -- remove pattern bindings   npm <- noPat m +  -- run expandPropGuards+  epgm <- expandPropGuards npm+   -- rename everything-  renMod <- renameModule npm+  renMod <- renameModule epgm ++{-+  -- 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   -- prelude, we have to generate the map from the renaming environment, as we   -- don't have the interface yet.@@ -453,21 +621,22 @@               else getPrimMap    -- typecheck-  let act = TCAction { tcAction = how-                     , tcLinter = moduleLinter (P.thing (P.mName m))+  let act = TCAction { tcAction = T.tcModule+                     , tcLinter = tcTopEntitytLinter (P.thing (P.mName m))                      , tcPrims  = prims }  -  tcm0 <- typecheck act (R.rmModule renMod) noIfaceParams (R.rmImported renMod)--  let tcm = tcm0 -- fromMaybe tcm0 (addModParams tcm0)+  tcm <- typecheck act (R.rmModule renMod) NoParams (R.rmImported renMod) -  rewMod <- liftSupply (`rewModule` tcm)+  rewMod <- case tcm of+              T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)+              T.TCTopSignature {} -> pure tcm   pure (R.rmInScope renMod,rewMod)  data TCLinter o = TCLinter   { lintCheck ::-      o -> T.InferInput -> Either (Range, TcSanity.Error) [TcSanity.ProofObligation]+      o -> T.InferInput ->+                    Either (Range, TcSanity.Error) [TcSanity.ProofObligation]   , lintModule :: Maybe P.ModName   } @@ -478,7 +647,8 @@       case TcSanity.tcExpr i e' of         Left err     -> Left err         Right (s1,os)-          | TcSanity.same s s1  -> Right os+          | TcSanity.SameIf os' <- TcSanity.same s s1 ->+                                        Right (map T.tMono os' ++ os)           | otherwise -> Left ( fromMaybe emptyRange (getLoc e')                               , TcSanity.TypeMismatch "exprLinter" s s1                               )@@ -502,6 +672,17 @@   , lintModule  = Just m   } +tcTopEntitytLinter :: P.ModName -> TCLinter T.TCTopEntity+tcTopEntitytLinter m = TCLinter+  { lintCheck   = \m' i -> case m' of+                             T.TCTopModule mo ->+                               lintCheck (moduleLinter m) mo i+                             T.TCTopSignature {} -> Right []+                                -- XXX: what can we lint about module interfaces+  , lintModule  = Just m+  }++ type Act i o = i -> T.InferInput -> IO (T.InferOutput o)  data TCAction i o = TCAction@@ -511,8 +692,8 @@   }  typecheck ::-  (Show i, Show o, HasLoc i) => TCAction i o -> i ->-                                  IfaceParams -> IfaceDecls -> ModuleM o+  (Show i, Show o, HasLoc i) =>+  TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o typecheck act i params env = do    let range = fromMaybe emptyRange (getLoc i)@@ -531,8 +712,12 @@            CoreLint   -> case lintCheck (tcLinter act) o input of                            Right as ->                              let ppIt l = mapM_ (logPrint l . T.pp)-                             in withLogger ppIt as-                           Left err -> panic "Core lint failed:" [show err]+                             in withLogger ppIt (TcSanity.onlyNonTrivial as)+                           Left (loc,err) ->+                            panic "Core lint failed:"+                              [ "Location: " ++ show (T.pp loc)+                              , show (T.pp err)+                              ]          return o      T.InferFailed nameMap warns errs ->@@ -540,8 +725,9 @@          typeCheckingFailed nameMap errs  -- | Generate input for the typechecker.-genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput-genInferInput r prims params env' = do+genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls ->+                                                          ModuleM T.InferInput+genInferInput r prims params env = do   seeds <- getNameSeeds   monoBinds <- getMonoBinds   solver <- getTCSolver@@ -549,25 +735,29 @@   searchPath <- getSearchPath   callStacks <- getCallStacks -  -- TODO: include the environment needed by the module-  let env = flatPublicDecls env'-            -- XXX: we should really just pass this directly+  topMods <- getAllLoaded+  topSigs <- getAllLoadedSignatures+   return T.InferInput-    { T.inpRange     = r-    , T.inpVars      = Map.map ifDeclSig (ifDecls env)-    , T.inpTSyns     = ifTySyns env-    , T.inpNewtypes  = ifNewtypes env-    , T.inpAbstractTypes = ifAbstractTypes env-    , T.inpNameSeeds = seeds-    , T.inpMonoBinds = monoBinds-    , T.inpCallStacks = callStacks-    , T.inpSearchPath = searchPath-    , T.inpSupply    = supply-    , T.inpPrimNames = prims-    , T.inpParamTypes       = ifParamTypes params-    , T.inpParamConstraints = ifParamConstraints params-    , T.inpParamFuns        = ifParamFuns params+    { T.inpRange            = r+    , T.inpVars             = Map.map ifDeclSig (ifDecls env)+    , T.inpTSyns            = ifTySyns env+    , T.inpNewtypes         = ifNewtypes env+    , T.inpAbstractTypes    = ifAbstractTypes env+    , T.inpSignatures       = ifSignatures env+    , T.inpNameSeeds        = seeds+    , T.inpMonoBinds        = monoBinds+    , T.inpCallStacks       = callStacks+    , T.inpSearchPath       = searchPath+    , T.inpSupply           = supply+    , T.inpParams           = case params of+                                NoParams -> T.allParamNames mempty+                                FunctorParams ps -> T.allParamNames ps+                                InterfaceParams ps -> ps+    , T.inpPrimNames        = prims     , T.inpSolver           = solver+    , T.inpTopModules       = topMods+    , T.inpTopSignatures    = topSigs     }  @@ -585,6 +775,22 @@   let ?callStacks = callStacks    io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)++benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats+benchmarkExpr period e = do+  env <- getEvalEnv+  denv <- getDynEnv+  evopts <- getEvalOptsAction+  let env' = env <> deEnv denv+  let tbl = Concrete.primTable evopts+  let ?evalPrim = \i -> Right <$> Map.lookup i tbl+  let ?range = emptyRange+  callStacks <- getCallStacks+  let ?callStacks = callStacks++  let eval expr = E.runEval mempty $+        E.evalExpr Concrete env' expr >>= E.forceValue+  io $ benchmark period eval e  evalDecls :: [T.DeclGroup] -> ModuleM () evalDecls dgs = do

@@ -0,0 +1,434 @@+{-# Language BlockArguments #-}+{-# Language RecordWildCards #-}+{-# Language FlexibleInstances #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+module Cryptol.ModuleSystem.Binds+  ( BindsNames+  , TopDef(..)+  , Mod(..)+  , ModKind(..)+  , modNested+  , modBuilder+  , topModuleDefs+  , topDeclsDefs+  , newModParam+  , InModule(..)+  , ifaceToMod+  , ifaceSigToMod+  , modToMap+  , defsOf+  ) where++import Data.Map(Map)+import qualified Data.Map as Map+import Data.Set(Set)+import qualified Data.Set as Set+import Data.Maybe(fromMaybe)+import Control.Monad(foldM)+import qualified MonadLib as M++import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.Ident(allNamespaces)+import Cryptol.Parser.Position+import Cryptol.Parser.Name(isGeneratedName)+import Cryptol.Parser.AST+import Cryptol.ModuleSystem.Exports(exportedDecls,exported)+import Cryptol.ModuleSystem.Renamer.Error+import Cryptol.ModuleSystem.Name+import Cryptol.ModuleSystem.Names+import Cryptol.ModuleSystem.NamingEnv+import Cryptol.ModuleSystem.Interface+import Cryptol.TypeCheck.Type(ModParamNames(..))++++data TopDef = TopMod ModName (Mod ())+            | TopInst ModName (ImpName PName) (ModuleInstanceArgs PName)++-- | Things defined by a module+data Mod a = Mod+  { modImports   :: [ ImportG (ImpName PName) ]+  , modKind      :: ModKind+  , modInstances :: Map Name (ImpName PName, ModuleInstanceArgs PName)+  , modMods      :: Map Name (Mod a) -- ^ this includes signatures++  , modDefines   :: NamingEnv+    {- ^ Things defined by this module.  Note the for normal modules we+    really just need the public names, however for things within+    functors we need all defined names, so that we can generate fresh+    names in instantiations -}++  , modPublic    :: !(Set Name)+    -- ^ These are the exported names++  , modState     :: a+    {- ^ Used in the import loop to track the current state of processing.+         The reason this is here, rather than just having a pair in the+         other algorithm is because this type is recursive (for nested modules)+         and it is conveninet to keep track for all modules at once -}+  }++modNested :: Mod a -> Set Name+modNested m = Set.unions [ Map.keysSet (modInstances m)+                         , Map.keysSet (modMods m)+                         ]++instance Functor Mod where+  fmap f m = m { modState = f (modState m)+               , modMods  = fmap f <$> modMods m+               }++-- | Generate a map from this module and all modules nested in it.+modToMap ::+  ImpName Name -> Mod () ->+  Map (ImpName Name) (Mod ()) -> Map (ImpName Name) (Mod ())+modToMap x m mp = Map.insert x m (Map.foldrWithKey add mp (modMods m))+  where+  add n = modToMap (ImpNested n)++-- | Make a `Mod` from the public declarations in an interface.+-- This is used to handle imports.+ifaceToMod :: IfaceG name -> Mod ()+ifaceToMod iface = ifaceNamesToMod iface (ifaceIsFunctor iface) (ifNames iface)++ifaceNamesToMod :: IfaceG topname -> Bool -> IfaceNames name -> Mod ()+ifaceNamesToMod iface params names =+  Mod+    { modKind    = if params then AFunctor else AModule+    , modMods    = (ifaceNamesToMod iface False <$> ifModules decls)+                   `Map.union`+                   (ifaceToMod <$> ifFunctors decls)+                   `Map.union`+                   (ifaceSigToMod <$> ifSignatures decls)+    , modDefines = namingEnvFromNames defs+    , modPublic  = ifsPublic names++    , modImports   = []+    , modInstances = mempty+    , modState     = ()+    }+  where+  defs      = ifsDefines names+  isLocal x = x `Set.member` defs+  decls     = filterIfaceDecls isLocal (ifDefines iface)+++ifaceSigToMod :: ModParamNames -> Mod ()+ifaceSigToMod ps = Mod+  { modImports   = []+  , modKind      = ASignature+  , modInstances = mempty+  , modMods      = mempty+  , modDefines   = env+  , modPublic    = namingEnvNames env+  , modState     = ()+  }+  where+  env = modParamsNamingEnv ps+++++++type ModBuilder = SupplyT (M.StateT [RenamerError] M.Id)++modBuilder :: ModBuilder a -> Supply -> ((a, [RenamerError]),Supply)+modBuilder m s = ((a,errs),s1)+  where ((a,s1),errs) = M.runId (M.runStateT [] (runSupplyT s m))++defErr :: RenamerError -> ModBuilder ()+defErr a = M.lift (M.sets_ (a:))++defNames :: BuildNamingEnv -> ModBuilder NamingEnv+defNames b = liftSupply \s -> M.runId (runSupplyT s (runBuild b))+++topModuleDefs :: Module PName -> ModBuilder TopDef+topModuleDefs m =+  case mDef m of+    NormalModule ds -> TopMod mname <$> declsToMod (Just (TopModule mname)) ds+    FunctorInstance f as _ -> pure (TopInst mname (thing f) as)+    InterfaceModule s -> TopMod mname <$> sigToMod (TopModule mname) s+  where+  mname = thing (mName m)++topDeclsDefs :: ModPath -> [TopDecl PName] -> ModBuilder (Mod ())+topDeclsDefs = declsToMod . Just++sigToMod :: ModPath -> Signature PName -> ModBuilder (Mod ())+sigToMod mp sig =+  do env <- defNames (signatureDefs mp sig)+     pure Mod { modImports   = map thing (sigImports sig)+              , modKind      = ASignature+              , modInstances = mempty+              , modMods      = mempty+              , modDefines   = env+              , modPublic    = namingEnvNames env+              , modState     = ()+              }++++declsToMod :: Maybe ModPath -> [TopDecl PName] -> ModBuilder (Mod ())+declsToMod mbPath ds =+  do defs <- defNames (foldMap (namingEnv . InModule mbPath) ds)+     let expSpec = exportedDecls ds+     let pub     = Set.fromList+                     [ name+                     | ns    <- allNamespaces+                     , pname <- Set.toList (exported ns expSpec)+                     , name  <- lookupListNS ns pname defs+                     ]++     case findAmbig defs of+       bad@(_ : _) : _ ->+         -- defErr (MultipleDefinitions mbPath (nameIdent f) (map nameLoc bad))+         defErr (OverlappingSyms bad)+       _ -> pure ()++     let mo = Mod { modImports      = [ thing i | DImport i <- ds ]+                  , modKind         = if any isParamDecl ds+                                         then AFunctor else AModule+                  , modInstances    = mempty+                  , modMods         = mempty+                  , modDefines      = defs+                  , modPublic       = pub+                  , modState        = ()+                  }++     foldM (checkNest defs) mo ds++  where+  checkNest defs mo d =+    case d of+      DModule tl ->+        do let NestedModule nmod = tlValue tl+               pname = thing (mName nmod)+               name  = case lookupNS NSModule pname defs of+                         Just xs -> anyOne xs+                         _ -> panic "declsToMod" ["undefined name", show pname]+           case mbPath of+             Nothing ->+               do defErr (UnexpectedNest (srcRange (mName nmod)) pname)+                  pure mo+             Just path ->+                case mDef nmod of++                   NormalModule xs ->+                     do m <- declsToMod (Just (Nested path (nameIdent name))) xs+                        pure mo { modMods = Map.insert name m (modMods mo) }++                   FunctorInstance f args _ ->+                      pure mo { modInstances = Map.insert name (thing f, args)+                                                    (modInstances mo) }++                   InterfaceModule sig ->+                      do m <- sigToMod (Nested path (nameIdent name)) sig+                         pure mo { modMods = Map.insert name m (modMods mo) }+++      _ -> pure mo++++-- | These are the names "owned" by the signature.  These names are+-- used when resolving the signature.  They are also used to figure out what+-- names to instantuate when the signature is used.+signatureDefs :: ModPath -> Signature PName -> BuildNamingEnv+signatureDefs m sig =+     mconcat [ namingEnv (InModule loc p) | p <- sigTypeParams sig ]+  <> mconcat [ namingEnv (InModule loc p) | p <- sigFunParams sig ]+  <> mconcat [ namingEnv (InModule loc p) | p <- sigDecls sig ]+  where+  loc = Just m+--------------------------------------------------------------------------------+++++--------------------------------------------------------------------------------+-- Computes the names introduced by various declarations.++-- | Things that define exported names.+class BindsNames a where+  namingEnv :: a -> BuildNamingEnv++newtype BuildNamingEnv = BuildNamingEnv { runBuild :: SupplyT M.Id NamingEnv }++buildNamingEnv :: BuildNamingEnv -> Supply -> (NamingEnv,Supply)+buildNamingEnv b supply = M.runId $ runSupplyT supply $ runBuild b++-- | Generate a 'NamingEnv' using an explicit supply.+defsOf :: BindsNames a => a -> Supply -> (NamingEnv,Supply)+defsOf = buildNamingEnv . namingEnv++instance Semigroup BuildNamingEnv where+  BuildNamingEnv a <> BuildNamingEnv b = BuildNamingEnv $+    do x <- a+       y <- b+       return (mappend x y)++instance Monoid BuildNamingEnv where+  mempty = BuildNamingEnv (pure mempty)++  mappend = (<>)++  mconcat bs = BuildNamingEnv $+    do ns <- sequence (map runBuild bs)+       return (mconcat ns)++instance BindsNames NamingEnv where+  namingEnv env = BuildNamingEnv (return env)+  {-# INLINE namingEnv #-}++instance BindsNames a => BindsNames (Maybe a) where+  namingEnv = foldMap namingEnv+  {-# INLINE namingEnv #-}++instance BindsNames a => BindsNames [a] where+  namingEnv = foldMap namingEnv+  {-# INLINE namingEnv #-}++-- | Generate a type renaming environment from the parameters that are bound by+-- this schema.+instance BindsNames (Schema PName) where+  namingEnv (Forall ps _ _ _) = foldMap namingEnv ps+  {-# INLINE namingEnv #-}++++-- | Introduce the name+instance BindsNames (InModule (Bind PName)) where+  namingEnv (InModule mb b) = BuildNamingEnv $+    do let Located { .. } = bName b+       n <- case mb of+              Just m  -> newTop NSValue m thing (bFixity b) srcRange+              Nothing -> newLocal NSValue thing srcRange -- local fixitiies?++       return (singletonNS NSValue thing n)++-- | Generate the naming environment for a type parameter.+instance BindsNames (TParam PName) where+  namingEnv TParam { .. } = BuildNamingEnv $+    do let range = fromMaybe emptyRange tpRange+       n <- newLocal NSType tpName range+       return (singletonNS NSType tpName n)+++instance BindsNames (InModule (TopDecl PName)) where+  namingEnv (InModule ns td) =+    case td of+      Decl d           -> namingEnv (InModule ns (tlValue d))+      DPrimType d      -> namingEnv (InModule ns (tlValue d))+      TDNewtype d      -> namingEnv (InModule ns (tlValue d))+      DParamDecl {}    -> mempty+      Include _        -> mempty+      DImport {}       -> mempty -- see 'openLoop' in the renamer+      DModule m        -> namingEnv (InModule ns (tlValue m))+      DModParam {}     -> mempty -- shouldn't happen+      DInterfaceConstraint {} -> mempty+        -- handled in the renamer as we need to resolve+        -- the signature name first (similar to import)+++instance BindsNames (InModule (NestedModule PName)) where+  namingEnv (InModule ~(Just m) (NestedModule mdef)) = BuildNamingEnv $+    do let pnmame = mName mdef+       nm   <- newTop NSModule m (thing pnmame) Nothing (srcRange pnmame)+       pure (singletonNS NSModule (thing pnmame) nm)++instance BindsNames (InModule (PrimType PName)) where+  namingEnv (InModule ~(Just m) PrimType { .. }) =+    BuildNamingEnv $+      do let Located { .. } = primTName+         nm <- newTop NSType m thing primTFixity srcRange+         pure (singletonNS NSType thing nm)++instance BindsNames (InModule (ParameterFun PName)) where+  namingEnv (InModule ~(Just ns) ParameterFun { .. }) = BuildNamingEnv $+    do let Located { .. } = pfName+       ntName <- newTop NSValue ns thing pfFixity srcRange+       return (singletonNS NSValue thing ntName)++instance BindsNames (InModule (ParameterType PName)) where+  namingEnv (InModule ~(Just ns) ParameterType { .. }) = BuildNamingEnv $+    -- XXX: we don't seem to have a fixity environment at the type level+    do let Located { .. } = ptName+       ntName <- newTop NSType ns thing Nothing srcRange+       return (singletonNS NSType thing ntName)++instance BindsNames (InModule (Newtype PName)) where+  namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $+    do let Located { .. } = nName+       ntName    <- newTop NSType  ns thing Nothing srcRange+       ntConName <- newTop NSValue ns thing Nothing srcRange+       return (singletonNS NSType thing ntName `mappend`+               singletonNS NSValue thing ntConName)++-- | The naming environment for a single declaration.+instance BindsNames (InModule (Decl PName)) where+  namingEnv (InModule pfx d) = case d of+    DBind b                 -> namingEnv (InModule pfx b)+    DSignature ns _sig      -> foldMap qualBind ns+    DPragma ns _p           -> foldMap qualBind ns+    DType syn               -> qualType (tsName syn) (tsFixity syn)+    DProp syn               -> qualType (psName syn) (psFixity syn)+    DLocated d' _           -> namingEnv (InModule pfx d')+    DRec {}                 -> panic "namingEnv" [ "DRec" ]+    DPatBind _pat _e        -> panic "namingEnv" ["Unexpected pattern binding"]+    DFixity{}               -> panic "namingEnv" ["Unexpected fixity declaration"]++    where++    mkName ns ln fx = case pfx of+                        Just m  -> newTop ns m (thing ln) fx (srcRange ln)+                        Nothing -> newLocal ns (thing ln) (srcRange ln)++    qualBind ln = BuildNamingEnv $+      do n <- mkName NSValue ln Nothing+         return (singletonNS NSValue (thing ln) n)++    qualType ln f = BuildNamingEnv $+      do n <- mkName NSType ln f+         return (singletonNS NSType (thing ln) n)++instance BindsNames (InModule (SigDecl PName)) where+  namingEnv (InModule m d) =+    case d of+      SigTySyn ts _    -> namingEnv (InModule m (DType ts))+      SigPropSyn ps _  -> namingEnv (InModule m (DProp ps))+++++--------------------------------------------------------------------------------+-- Helpers++newTop ::+  FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name+newTop ns m thing fx rng =+  liftSupply (mkDeclared ns m src (getIdent thing) fx rng)+  where src = if isGeneratedName thing then SystemName else UserName++newLocal :: FreshM m => Namespace -> PName -> Range -> m Name+newLocal ns thing rng = liftSupply (mkLocal ns (getIdent thing) rng)++-- | Given a name in a signature, make a name for the parameter corresponding+-- to the signature.+newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name+newModParam m i rng n = liftSupply (mkModParam m i rng n)+++{- | Do something in the context of a module.+If `Nothing` than we are working with a local declaration.+Otherwise we are at the top-level of the given module.++By wrapping types with this, we can pass the module path+to methods that need the extra information. -}+data InModule a = InModule (Maybe ModPath) a+                  deriving (Functor,Traversable,Foldable,Show)+++

@@ -7,17 +7,20 @@ -- Portability :  portable  {-# LANGUAGE CPP #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-} module Cryptol.ModuleSystem.Env where  #ifndef RELOCATABLE import Paths_cryptol (getDataDir) #endif +import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc, getForeignSrcPath) import Cryptol.Eval (EvalEnv) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface@@ -34,13 +37,16 @@ import qualified Control.Exception as X import Data.Function (on) import Data.Set(Set)+import qualified Data.Set as Set import Data.Map (Map) import qualified Data.Map as Map import Data.Semigroup+import Data.Maybe(fromMaybe) import System.Directory (getAppUserDataDirectory, getCurrentDirectory) import System.Environment(getExecutablePath) import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory) import qualified Data.List as List+import Data.Foldable  import GHC.Generics (Generic) import Control.DeepSeq@@ -99,14 +105,19 @@               | CoreLint          -- ^ Run core lint   deriving (Generic, NFData) -resetModuleEnv :: ModuleEnv -> ModuleEnv-resetModuleEnv env = env-  { meLoadedModules = mempty-  , meNameSeeds     = T.nameSeeds-  , meEvalEnv       = mempty-  , meFocusedModule = Nothing-  , meDynEnv        = mempty-  }+resetModuleEnv :: ModuleEnv -> IO ModuleEnv+resetModuleEnv env = do+  for_ (getLoadedModules $ meLoadedModules env) $ \lm ->+    case lmForeignSrc (lmData lm) of+      Just fsrc -> unloadForeignSrc fsrc+      _         -> pure ()+  pure env+    { meLoadedModules = mempty+    , meNameSeeds     = T.nameSeeds+    , meEvalEnv       = mempty+    , meFocusedModule = Nothing+    , meDynEnv        = mempty+    }  initialModuleEnv :: IO ModuleEnv initialModuleEnv = do@@ -171,9 +182,9 @@ loadedNonParamModules :: ModuleEnv -> [T.Module] loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules -loadedNewtypes :: ModuleEnv -> Map Name IfaceNewtype+loadedNewtypes :: ModuleEnv -> Map Name T.Newtype loadedNewtypes menv = Map.unions-   [ ifNewtypes (ifPublic i) <> ifNewtypes (ifPrivate i)+   [ ifNewtypes (ifDefines i) <> ifNewtypes (ifDefines i)    | i <- map lmInterface (getLoadedModules (meLoadedModules menv))    ] @@ -184,10 +195,22 @@ allDeclGroups :: ModuleEnv -> [T.DeclGroup] allDeclGroups = concatMap T.mDecls . loadedNonParamModules +data ModContextParams =+    InterfaceParams T.ModParamNames+  | FunctorParams T.FunctorParams+  | NoParams++modContextParamNames :: ModContextParams -> T.ModParamNames+modContextParamNames mp =+  case mp of+    InterfaceParams ps -> ps+    FunctorParams ps   -> T.allParamNames ps+    NoParams           -> T.allParamNames mempty+ -- | Contains enough information to browse what's in scope, -- or type check new expressions. data ModContext = ModContext-  { mctxParams          :: IfaceParams+  { mctxParams          :: ModContextParams -- T.FunctorParams   , mctxExported        :: Set Name   , mctxDecls           :: IfaceDecls     -- ^ Should contain at least names in NamingEnv, but may have more@@ -199,7 +222,7 @@ -- This instance is a bit bogus.  It is mostly used to add the dynamic -- environemnt to an existing module, and it makes sense for that use case. instance Semigroup ModContext where-  x <> y = ModContext { mctxParams   = jnParams (mctxParams x) (mctxParams y)+  x <> y = ModContext { mctxParams   = jnPs (mctxParams x) (mctxParams y)                       , mctxExported = mctxExported x <> mctxExported y                       , mctxDecls    = mctxDecls x  <> mctxDecls  y                       , mctxNames    = names@@ -208,14 +231,15 @@        where       names = mctxNames x `R.shadowing` mctxNames y-      jnParams a b-        | isEmptyIfaceParams a = b-        | isEmptyIfaceParams b = a-        | otherwise =-          panic "ModContext" [ "Cannot combined 2 parameterized contexts" ]+      jnPs as bs =+        case (as,bs) of+          (NoParams,_) -> bs+          (_,NoParams) -> as+          (FunctorParams xs, FunctorParams ys) -> FunctorParams (xs <> ys)+          _ -> panic "(<>) @ ModContext" ["Can't combine parameters"]  instance Monoid ModContext where-  mempty = ModContext { mctxParams   = noIfaceParams+  mempty = ModContext { mctxParams   = NoParams                       , mctxDecls    = mempty                       , mctxExported = mempty                       , mctxNames    = mempty@@ -229,16 +253,36 @@   do lm <- lookupModule mname me      let localIface  = lmInterface lm          localNames  = lmNamingEnv lm-         loadedDecls = map (ifPublic . lmInterface)++         -- XXX: do we want only public ones here?+         loadedDecls = map (ifDefines . lmInterface)                      $ getLoadedModules (meLoadedModules me)++         params = ifParams localIface      pure ModContext-       { mctxParams   = ifParams localIface-       , mctxExported = ifaceDeclsNames (ifPublic localIface)-       , mctxDecls    = mconcat (ifPrivate localIface : loadedDecls)+       { mctxParams   = if Map.null params then NoParams+                                           else FunctorParams params+       , mctxExported = ifsPublic (ifNames localIface)+       , mctxDecls    = mconcat (ifDefines localIface : loadedDecls)        , mctxNames    = localNames        , mctxNameDisp = R.toNameDisp localNames        }+  `mplus`+  do lm <- lookupSignature mname me+     let localNames  = lmNamingEnv lm+         -- XXX: do we want only public ones here?+         loadedDecls = map (ifDefines . lmInterface)+                     $ getLoadedModules (meLoadedModules me)+     pure ModContext+       { mctxParams   = InterfaceParams (lmData lm)+       , mctxExported = Set.empty+       , mctxDecls    = mconcat loadedDecls+       , mctxNames    = localNames+       , mctxNameDisp = R.toNameDisp localNames+       } ++ dynModContext :: ModuleEnv -> ModContext dynModContext me = mempty { mctxNames    = dynNames                           , mctxNameDisp = R.toNameDisp dynNames@@ -277,6 +321,17 @@       (InMem a _, InMem b _) -> a == b       _ -> False +-- | In-memory things are compared by label.+instance Ord ModulePath where+  compare p1 p2 =+    case (p1,p2) of+      (InFile x, InFile y)   -> compare x y+      (InMem a _, InMem b _) -> compare a b+      (InMem {}, InFile {})  -> LT+      (InFile {}, InMem {})  -> GT+++ instance PP ModulePath where   ppPrec _ e =     case e of@@ -303,24 +358,49 @@   , lmLoadedParamModules :: [LoadedModule]     -- ^ Loaded parameterized modules. +  , lmLoadedSignatures :: ![LoadedSignature]+   } deriving (Show, Generic, NFData) +data LoadedEntity =+    ALoadedModule LoadedModule+  | ALoadedFunctor LoadedModule+  | ALoadedInterface LoadedSignature++getLoadedEntities ::+  LoadedModules -> Map ModName LoadedEntity+getLoadedEntities lm =+  Map.fromList $ [ (lmName x, ALoadedModule x) | x <- lmLoadedModules lm ] +++                 [ (lmName x, ALoadedFunctor x) | x <- lmLoadedParamModules lm ] +++                 [ (lmName x, ALoadedInterface x) | x <- lmLoadedSignatures lm ]+ getLoadedModules :: LoadedModules -> [LoadedModule] getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x +getLoadedNames :: LoadedModules -> Set ModName+getLoadedNames lm = Set.fromList+                  $ map lmName (lmLoadedModules lm)+                 ++ map lmName (lmLoadedParamModules lm)+                 ++ map lmName (lmLoadedSignatures lm)+ instance Semigroup LoadedModules where   l <> r = LoadedModules     { lmLoadedModules = List.unionBy ((==) `on` lmName)                                       (lmLoadedModules l) (lmLoadedModules r)-    , lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r }+    , lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r+    , lmLoadedSignatures   = lmLoadedSignatures l ++ lmLoadedSignatures r+    }  instance Monoid LoadedModules where   mempty = LoadedModules { lmLoadedModules = []                          , lmLoadedParamModules = []+                         , lmLoadedSignatures = []                          }   mappend = (<>) -data LoadedModule = LoadedModule+-- | A generic type for loaded things.+-- The things can be either modules or signatures.+data LoadedModuleG a = LoadedModule   { lmName              :: ModName     -- ^ The name of this module.  Should match what's in 'lmModule' @@ -335,36 +415,94 @@   , lmNamingEnv         :: !R.NamingEnv     -- ^ What's in scope in this module -  , lmInterface         :: Iface+  , lmFileInfo          :: !FileInfo++  , lmData              :: a+  } deriving (Show, Generic, NFData)++type LoadedModule = LoadedModuleG LoadedModuleData++lmModule :: LoadedModule -> T.Module+lmModule = lmdModule . lmData++lmInterface :: LoadedModule -> Iface+lmInterface = lmdInterface . lmData++data LoadedModuleData = LoadedModuleData+  { lmdInterface         :: Iface     -- ^ The module's interface. -  , lmModule            :: T.Module+  , lmdModule            :: T.Module     -- ^ The actual type-checked module -  , lmFingerprint       :: Fingerprint+  , lmForeignSrc        :: Maybe ForeignSrc+    -- ^ The dynamically loaded source for any foreign functions in the module   } deriving (Show, Generic, NFData) +type LoadedSignature = LoadedModuleG T.ModParamNames++ -- | Has this module been loaded already. isLoaded :: ModName -> LoadedModules -> Bool-isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)+isLoaded mn lm = mn `Set.member` getLoadedNames lm  -- | Is this a loaded parameterized module. isLoadedParamMod :: ModName -> LoadedModules -> Bool isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln) +-- | Is this a loaded interface module.+isLoadedInterface :: ModName -> LoadedModules -> Bool+isLoadedInterface mn ln = any ((mn ==) . lmName) (lmLoadedSignatures ln)++++lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG T.TCTopEntity)+lookupTCEntity m env =+  case lookupModule m env of+    Just lm -> pure lm { lmData = T.TCTopModule (lmModule lm) }+    Nothing ->+      do lm <- lookupSignature m env+         pure lm { lmData = T.TCTopSignature m (lmData lm) }+ -- | Try to find a previously loaded module lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules   where   search how = List.find ((mn ==) . lmName) (how (meLoadedModules me)) +lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature+lookupSignature mn me =+  List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me)) +addLoadedSignature ::+  ModulePath -> String ->+  FileInfo ->+  R.NamingEnv ->+  ModName -> T.ModParamNames ->+  LoadedModules -> LoadedModules+addLoadedSignature path ident fi nameEnv nm si lm+  | isLoaded nm lm = lm+  | otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }+  where+  loaded = LoadedModule+            { lmName        = nm+            , lmFilePath    = path+            , lmModuleId    = ident+            , lmNamingEnv   = nameEnv+            , lmData        = si+            , lmFileInfo    = fi+            }+ -- | Add a freshly loaded module.  If it was previously loaded, then -- the new version is ignored. addLoadedModule ::-  ModulePath -> String -> Fingerprint -> R.NamingEnv -> T.Module ->-  LoadedModules -> LoadedModules-addLoadedModule path ident fp nameEnv tm lm+  ModulePath ->+  String ->+  FileInfo ->+  R.NamingEnv ->+  Maybe ForeignSrc ->+  T.Module -> LoadedModules -> LoadedModules+addLoadedModule path ident fi nameEnv fsrc tm lm   | isLoaded (T.mName tm) lm  = lm   | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :                                                 lmLoadedParamModules lm }@@ -376,21 +514,53 @@     , lmFilePath        = path     , lmModuleId        = ident     , lmNamingEnv       = nameEnv-    , lmInterface       = T.genIface tm-    , lmModule          = tm-    , lmFingerprint     = fp+    , lmData            = LoadedModuleData+                             { lmdInterface = T.genIface tm+                             , lmdModule    = tm+                             , lmForeignSrc = fsrc+                             }+    , lmFileInfo        = fi     }  -- | Remove a previously loaded module. -- Note that this removes exactly the modules specified by the predicate. -- One should be carfule to preserve the invariant on 'LoadedModules'.-removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules+removeLoadedModule ::+  (forall a. LoadedModuleG a -> Bool) -> LoadedModules -> LoadedModules removeLoadedModule rm lm =   LoadedModules-    { lmLoadedModules = filter (not . rm) (lmLoadedModules lm)-    , lmLoadedParamModules = filter (not . rm) (lmLoadedParamModules lm)+    { lmLoadedModules       = filter (not . rm) (lmLoadedModules lm)+    , lmLoadedParamModules  = filter (not . rm) (lmLoadedParamModules lm)+    , lmLoadedSignatures    = filter (not . rm) (lmLoadedSignatures lm)     } +-- FileInfo --------------------------------------------------------------------++data FileInfo = FileInfo+  { fiFingerprint :: Fingerprint+  , fiIncludeDeps :: Set FilePath+  , fiImportDeps  :: Set ModName+  , fiForeignDeps :: Set FilePath+  } deriving (Show,Generic,NFData)+++fileInfo ::+  Fingerprint ->+  Set FilePath ->+  Set ModName ->+  Maybe ForeignSrc ->+  FileInfo+fileInfo fp incDeps impDeps fsrc =+  FileInfo+    { fiFingerprint = fp+    , fiIncludeDeps = incDeps+    , fiImportDeps  = impDeps+    , fiForeignDeps = fromMaybe Set.empty+                      do src <- fsrc+                         Set.singleton <$> getForeignSrcPath src+    }++ -- Dynamic Environments --------------------------------------------------------  -- | Extra information we need to carry around to dynamically extend@@ -433,6 +603,8 @@                , ifAbstractTypes = Map.empty                , ifDecls = decls                , ifModules = Map.empty+               , ifFunctors = Map.empty+               , ifSignatures = Map.empty                }   where     decls = mconcat

@@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE Safe #-} module Cryptol.ModuleSystem.Exports where  import Data.Set(Set)@@ -10,30 +11,32 @@ import GHC.Generics (Generic)  import Cryptol.Parser.AST-import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT)+import Cryptol.Parser.Names(namesD,tnamesD,namesNT,tnamesNT) import Cryptol.ModuleSystem.Name -modExports :: Ord name => ModuleG mname name -> ExportSpec name-modExports m = fold (concat [ exportedNames d | d <- mDecls m ])-+exportedDecls :: Ord name => [TopDecl name] -> ExportSpec name+exportedDecls ds = fold (concat [ exportedNames d | d <- ds ])  exportedNames :: Ord name => TopDecl name -> [ExportSpec name]-exportedNames (Decl td) = map exportBind  (names namesD td)-                       ++ map exportType (names tnamesD td)-exportedNames (DPrimType t) = [ exportType (thing . primTName <$> t) ]-exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)-exportedNames (Include {})  = []-exportedNames (DImport {}) = []-exportedNames (DParameterFun {}) = []-exportedNames (DParameterType {}) = []-exportedNames (DParameterConstraint {}) = []-exportedNames (DModule nested) =-  case tlValue nested of-    NestedModule x ->-      [exportName NSModule nested { tlValue = thing (mName x) }]+exportedNames decl =+    case decl of+      Decl td -> map exportBind  (names  namesD td)+              ++ map exportType (names tnamesD td)+      DPrimType t -> [ exportType (thing . primTName <$> t) ]+      TDNewtype nt -> map exportType (names tnamesNT nt) +++                      map exportBind (names namesNT nt)+      Include {}  -> []+      DImport {} -> []+      DParamDecl {} -> []+      DInterfaceConstraint {} -> []+      DModule nested ->+        case tlValue nested of+          NestedModule x ->+            [exportName NSModule nested { tlValue = thing (mName x) }]+      DModParam {} -> []+  where+  names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ] -names :: (a -> ([Located a'], b)) -> TopLevel a -> [TopLevel a']-names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ]   newtype ExportSpec name = ExportSpec (Map Namespace (Set name))@@ -53,6 +56,9 @@                          $ Map.singleton ns                          $ Set.singleton (tlValue n)   | otherwise = mempty++allExported :: Ord name => ExportSpec name -> Set name+allExported (ExportSpec mp) = Set.unions (Map.elems mp)  exported :: Namespace -> ExportSpec name -> Set name exported ns (ExportSpec mp) = Map.findWithDefault Set.empty ns mp

@@ -10,6 +10,7 @@   ( Fingerprint   , fingerprint   , fingerprintFile+  , fingerprintHexString   ) where  import Control.DeepSeq          (NFData (rnf))@@ -17,6 +18,7 @@ import Data.ByteString          (ByteString) import Control.Exception        (try) import qualified Data.ByteString as B+import qualified Data.Vector as Vector  newtype Fingerprint = Fingerprint ByteString   deriving (Eq, Show)@@ -37,3 +39,13 @@        case res :: Either IOError ByteString of          Left{}  -> Nothing          Right b -> Just $! fingerprint b++fingerprintHexString :: Fingerprint -> String+fingerprintHexString (Fingerprint bs) = B.foldr hex "" bs+  where+  digits   = Vector.fromList "0123456789ABCDEF"+  digit x  = digits Vector.! fromIntegral x+  hex b cs = let (x,y) = divMod b 16+             in digit x : digit y : cs++

@@ -1,325 +0,0 @@-{-# Language FlexibleInstances, PatternGuards #-}-{-# Language BlockArguments #-}--- | Assumes that local names do not shadow top level names.-module Cryptol.ModuleSystem.InstantiateModule-  ( instantiateModule-  ) where--import           Data.Set (Set)-import qualified Data.Set as Set-import           Data.Map (Map)-import qualified Data.Map as Map-import           MonadLib(ReaderT,runReaderT,ask)--import Cryptol.Utils.Panic(panic)-import Cryptol.Utils.Ident(ModName,modParamIdent)-import Cryptol.Parser.Position(Located(..))-import Cryptol.ModuleSystem.Name-import Cryptol.TypeCheck.AST-import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)-import Cryptol.TypeCheck.SimpType(tRebuild)--{--XXX: Should we simplify constraints in the instantiated modules?--If so, we also need to adjust the constraint parameters on terms appropriately,-especially when working with dictionaries.--}----- | Convert a module instantiation into a partial module.--- The resulting module is incomplete because it is missing the definitions--- from the instantiation.-instantiateModule :: FreshM m =>-                     Module           {- ^ Parametrized module -} ->-                     ModName          {- ^ Name of the new module -} ->-                     Map TParam Type  {- ^ Type params -} ->-                     Map Name Expr    {- ^ Value parameters -} ->-                     m (Name -> Name, [Located Prop], Module)-                     -- ^ Renaming, instantiated constraints, fresh module, new supply-instantiateModule func newName tpMap vpMap-  | not (null (mSubModules func)) =-      panic "instantiateModule"-        [ "XXX: we don't support functors with nested moduels yet." ]-  | otherwise  =-  runReaderT (TopModule newName) $-    do let oldVpNames = Map.keys vpMap-       newVpNames <- mapM freshParamName (Map.keys vpMap)-       let vpNames = Map.fromList (zip oldVpNames newVpNames)--       env <- computeEnv func tpMap vpNames-       let ren x = case nameNamespace x of-                     NSValue -> Map.findWithDefault x x (funNameMap env)-                     NSType  -> Map.findWithDefault x x (tyNameMap env)-                     NSModule -> x--       let rnMp :: Inst a => (a -> Name) -> Map Name a -> Map Name a-           rnMp f m = Map.fromList [ (f x, x) | a <- Map.elems m-                                              , let x = inst env a ]--           renamedExports  = inst env (mExports func)-           renamedTySyns   = rnMp tsName (mTySyns func)-           renamedNewtypes = rnMp ntName (mNewtypes func)-           renamedPrimTys  = rnMp atName (mPrimTypes func)--           su = listParamSubst (Map.toList (tyParamMap env))--           goals = map (fmap (apSubst su)) (mParamConstraints func)-           -- Constraints to discharge about the type instances--       let renamedDecls = inst env (mDecls func)-           paramDecls = map (mkParamDecl su vpNames) (Map.toList vpMap)--       return ( ren-              , goals-              , Module-                 { mName              = newName-                 , mExports           = renamedExports-                 , mImports           = mImports func-                 , mTySyns            = renamedTySyns-                 , mNewtypes          = renamedNewtypes-                 , mPrimTypes         = renamedPrimTys-                 , mParamTypes        = Map.empty-                 , mParamConstraints  = []-                 , mParamFuns         = Map.empty-                 , mDecls             = paramDecls ++ renamedDecls--                 , mSubModules        = mempty-                 , mFunctors          = mempty-                 } )--  where-  mkParamDecl su vpNames (x,e) =-      NonRecursive Decl-        { dName        = Map.findWithDefault (error "OOPS") x vpNames-        , dSignature   = apSubst su-                       $ mvpType-                       $ Map.findWithDefault (error "UUPS") x (mParamFuns func)-        , dDefinition  = DExpr e-        , dPragmas     = []      -- XXX: which if any pragmas?-        , dInfix       = False   -- XXX: get from parameter?-        , dFixity      = Nothing -- XXX: get from parameter-        , dDoc         = Nothing -- XXX: get from parametr(or instance?)-        }-------------------------------------------------------------------------------------- Things that need to be renamed--class Defines t where-  defines :: t -> Set Name--instance Defines t => Defines [t] where-  defines = Set.unions . map defines--instance Defines Decl where-  defines = Set.singleton . dName--instance Defines DeclGroup where-  defines d =-    case d of-      NonRecursive x -> defines x-      Recursive x    -> defines x-------------------------------------------------------------------------------------type InstM = ReaderT ModPath---- | Generate a new instance of a declared name.-freshenName :: FreshM m => Name -> InstM m Name-freshenName x =-  do m <- ask-     let sys = case nameInfo x of-                 Declared _ s -> s-                 _            -> UserName-     liftSupply (mkDeclared (nameNamespace x)-                             m sys (nameIdent x) (nameFixity x) (nameLoc x))--freshParamName :: FreshM m => Name -> InstM m Name-freshParamName x =-  do m <- ask-     let newName = modParamIdent (nameIdent x)-     liftSupply (mkDeclared (nameNamespace x)-                          m UserName newName (nameFixity x) (nameLoc x))------- | Compute renaming environment from a module instantiation.--- computeEnv :: ModInst -> InstM Env-computeEnv :: FreshM m =>-              Module {- ^ Functor being instantiated -} ->-              Map TParam Type {- replace type params by type -} ->-              Map Name Name {- replace value parameters by other names -} ->-              InstM m Env-computeEnv m tpMap vpMap =-  do tss <- mapM freshTy (Map.toList (mTySyns m))-     nts <- mapM freshTy (Map.toList (mNewtypes m))-     let tnMap = Map.fromList (tss ++ nts)--     defHere <- mapM mkVParam (Set.toList (defines (mDecls m)))-     let fnMap = Map.union vpMap (Map.fromList defHere)--     return Env { funNameMap  = fnMap-                , tyNameMap   = tnMap-                , tyParamMap  = tpMap-                }-  where-  freshTy (x,_) = do y <- freshenName x-                     return (x,y)--  mkVParam x = do y <- freshenName x-                  return (x,y)--------------------------------------------------------------------------------------- Do the renaming--data Env = Env-  { funNameMap  :: Map Name Name-  , tyNameMap   :: Map Name Name-  , tyParamMap  :: Map TParam Type-  } deriving Show---class Inst t where-  inst :: Env -> t -> t--instance Inst a => Inst [a] where-  inst env = map (inst env)--instance Inst Expr where-  inst env = go-    where-    go expr =-      case expr of-        EVar x -> case Map.lookup x (funNameMap env) of-                    Just y -> EVar y-                    _      -> expr--        ELocated r e              -> ELocated r (inst env e)-        EList xs t                -> EList (inst env xs) (inst env t)-        ETuple es                 -> ETuple (inst env es)-        ERec xs                   -> ERec (fmap go xs)-        ESel e s                  -> ESel (go e) s-        ESet ty e x v             -> ESet (inst env ty) (go e) x (go v)-        EIf e1 e2 e3              -> EIf (go e1) (go e2) (go e3)-        EComp t1 t2 e mss         -> EComp (inst env t1) (inst env t2)-                                           (go e)-                                           (inst env mss)-        ETAbs t e                 -> ETAbs t (go e)-        ETApp e t                 -> ETApp (go e) (inst env t)-        EApp e1 e2                -> EApp (go e1) (go e2)-        EAbs x t e                -> EAbs x (inst env t) (go e)-        EProofAbs p e             -> EProofAbs (inst env p) (go e)-        EProofApp e               -> EProofApp (go e)-        EWhere e ds               -> EWhere (go e) (inst env ds)---instance Inst DeclGroup where-  inst env dg =-    case dg of-      NonRecursive d -> NonRecursive (inst env d)-      Recursive ds   -> Recursive (inst env ds)--instance Inst DeclDef where-  inst env d =-    case d of-      DPrim   -> DPrim-      DExpr e -> DExpr (inst env e)--instance Inst Decl where-  inst env d = d { dSignature = inst env (dSignature d)-                 , dDefinition = inst env (dDefinition d)-                 , dName = Map.findWithDefault (dName d) (dName d)-                                                         (funNameMap env)-                 }--instance Inst Match where-  inst env m =-    case m of-      From x t1 t2 e -> From x (inst env t1) (inst env t2) (inst env e)-      Let d          -> Let (inst env d)--instance Inst Schema where-  inst env s = s { sProps = inst env (sProps s)-                 , sType  = inst env (sType s)-                 }--instance Inst Type where-  inst env ty =-    tRebuild $-    case ty of-      TCon tc ts    -> TCon (inst env tc) (inst env ts)-      TVar tv       ->-        case tv of-          TVBound tp | Just t <- Map.lookup tp (tyParamMap env) -> t-          _ -> ty-      TUser x ts t  -> TUser y (inst env ts) (inst env t)-        where y = Map.findWithDefault x x (tyNameMap env)-      TRec fs       -> TRec (fmap (inst env) fs)-      TNewtype nt ts -> TNewtype (inst env nt) (inst env ts)--instance Inst TCon where-  inst env tc =-    case tc of-      TC x -> TC (inst env x)-      _    -> tc--instance Inst TC where-  inst env tc =-    case tc of-      TCAbstract x -> TCAbstract (inst env x)-      _            -> tc--instance Inst UserTC where-  inst env (UserTC x t) = UserTC y t-    where y = Map.findWithDefault x x (tyNameMap env)--instance Inst (ExportSpec Name) where-  inst env (ExportSpec spec) = ExportSpec (Map.mapWithKey doNS spec)-    where-    doNS ns =-      case ns of-        NSType  -> Set.map \x -> Map.findWithDefault x x (tyNameMap env)-        NSValue -> Set.map \x -> Map.findWithDefault x x (funNameMap env)-        NSModule -> id---instance Inst TySyn where-  inst env ts = TySyn { tsName = instTyName env x-                      , tsParams = tsParams ts-                      , tsConstraints = inst env (tsConstraints ts)-                      , tsDef = inst env (tsDef ts)-                      , tsDoc = tsDoc ts-                      }-    where x = tsName ts--instance Inst Newtype where-  inst env nt = Newtype { ntName = instTyName env x-                        , ntParams = ntParams nt-                        , ntConstraints = inst env (ntConstraints nt)-                        , ntFields = fmap (inst env) (ntFields nt)-                        , ntDoc = ntDoc nt-                        }-    where x = ntName nt--instance Inst AbstractType where-  inst env a = AbstractType { atName    = instTyName env (atName a)-                            , atKind    = atKind a-                            , atCtrs    = case atCtrs a of-                                            (xs,ps) -> (xs, inst env ps)-                            , atFixitiy = atFixitiy a-                            , atDoc     = atDoc a-                            }--instTyName :: Env -> Name -> Name-instTyName env x = Map.findWithDefault x x (tyNameMap env)------

@@ -9,30 +9,28 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE Safe #-} module Cryptol.ModuleSystem.Interface (     Iface   , IfaceG(..)   , IfaceDecls(..)-  , IfaceTySyn, ifTySynName-  , IfaceNewtype   , IfaceDecl(..)-  , IfaceParams(..)+  , IfaceNames(..)+  , ifModName    , emptyIface   , ifacePrimMap-  , noIfaceParams-  , isEmptyIfaceParams+  , ifaceForgetName   , ifaceIsFunctor-  , flatPublicIface-  , flatPublicDecls   , filterIfaceDecls   , ifaceDeclsNames+  , ifaceOrigNameMap   ) where  import           Data.Set(Set) import qualified Data.Set as Set+import           Data.Map (Map) import qualified Data.Map as Map import           Data.Semigroup import           Data.Text (Text)@@ -44,74 +42,76 @@ import Prelude.Compat  import Cryptol.ModuleSystem.Name-import Cryptol.Utils.Ident (ModName)+import Cryptol.Utils.Ident (ModName, OrigName(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity) import Cryptol.Parser.AST(Pragma)-import Cryptol.Parser.Position(Located) import Cryptol.TypeCheck.Type +type Iface = IfaceG ModName --- | The resulting interface generated by a module that has been typechecked.-data IfaceG mname = Iface-  { ifModName   :: !mname       -- ^ Module name-  , ifPublic    :: IfaceDecls   -- ^ Exported definitions-  , ifPrivate   :: IfaceDecls   -- ^ Private defintiions-  , ifParams    :: IfaceParams  -- ^ Uninterpreted constants (aka module params)+-- | The interface repersenting a typecheck top-level module.+data IfaceG name = Iface+  { ifNames     :: IfaceNames name    -- ^ Info about names in this module+  , ifParams    :: FunctorParams      -- ^ Module parameters, if any+  , ifDefines   :: IfaceDecls         -- ^ All things defines in the module+                                      -- (includes nested definitions)   } deriving (Show, Generic, NFData) -ifaceIsFunctor :: IfaceG mname -> Bool-ifaceIsFunctor = not . isEmptyIfaceParams . ifParams---- | The public declarations in all modules, including nested--- The modules field contains public functors--- Assumes that we are not a functor.-flatPublicIface :: IfaceG mname -> IfaceDecls-flatPublicIface iface = flatPublicDecls (ifPublic iface)---flatPublicDecls :: IfaceDecls -> IfaceDecls-flatPublicDecls ifs = mconcat ( ifs { ifModules = fun }-                              : map flatPublicIface (Map.elems nofun)-                              )+-- | Remove the name of a module.  This is useful for dealing with collections+-- of modules, as in `Map (ImpName Name) (IfaceG ())`.+ifaceForgetName :: IfaceG name -> IfaceG ()+ifaceForgetName i = i { ifNames = newNames }+  where newNames = (ifNames i) { ifsName = () } -  where-  (fun,nofun) = Map.partition ifaceIsFunctor (ifModules ifs)+-- | Access the name of a module.+ifModName :: IfaceG name -> name+ifModName = ifsName . ifNames +-- | Information about the names in a module.+data IfaceNames name = IfaceNames+  { ifsName     :: name       -- ^ Name of this submodule+  , ifsNested   :: Set Name   -- ^ Things nested in this module+  , ifsDefines  :: Set Name   -- ^ Things defined in this module+  , ifsPublic   :: Set Name   -- ^ Subset of `ifsDefines` that is public+  , ifsDoc      :: !(Maybe Text) -- ^ Documentation+  } deriving (Show, Generic, NFData) -type Iface = IfaceG ModName+-- | Is this interface for a functor.+ifaceIsFunctor :: IfaceG name -> Bool+ifaceIsFunctor = not . Map.null . ifParams -emptyIface :: mname -> IfaceG mname+emptyIface :: ModName -> Iface emptyIface nm = Iface-  { ifModName = nm-  , ifPublic  = mempty-  , ifPrivate = mempty-  , ifParams  = noIfaceParams-  }--data IfaceParams = IfaceParams-  { ifParamTypes       :: Map.Map Name ModTParam-  , ifParamConstraints :: [Located Prop] -- ^ Constraints on param. types-  , ifParamFuns        :: Map.Map Name ModVParam-  } deriving (Show, Generic, NFData)--noIfaceParams :: IfaceParams-noIfaceParams = IfaceParams-  { ifParamTypes = Map.empty-  , ifParamConstraints = []-  , ifParamFuns = Map.empty+  { ifNames   = IfaceNames { ifsName    = nm+                           , ifsDefines = mempty+                           , ifsPublic  = mempty+                           , ifsNested  = mempty+                           , ifsDoc     = Nothing+                           }+  , ifParams  = mempty+  , ifDefines = mempty   } -isEmptyIfaceParams :: IfaceParams -> Bool-isEmptyIfaceParams IfaceParams { .. } =-  Map.null ifParamTypes && null ifParamConstraints && Map.null ifParamFuns-+-- | Declarations in a module.  Note that this includes things from nested+-- modules, but not things from nested functors, which are in `ifFunctors`. data IfaceDecls = IfaceDecls-  { ifTySyns        :: Map.Map Name IfaceTySyn-  , ifNewtypes      :: Map.Map Name IfaceNewtype-  , ifAbstractTypes :: Map.Map Name IfaceAbstractType+  { ifTySyns        :: Map.Map Name TySyn+  , ifNewtypes      :: Map.Map Name Newtype+  , ifAbstractTypes :: Map.Map Name AbstractType   , ifDecls         :: Map.Map Name IfaceDecl-  , ifModules       :: !(Map.Map Name (IfaceG Name))+  , ifModules       :: !(Map.Map Name (IfaceNames Name))+  , ifSignatures    :: !(Map.Map Name ModParamNames)+  , ifFunctors      :: !(Map.Map Name (IfaceG Name))+    {- ^ XXX: Maybe arg info?+    Also, with the current implementation we aim to complete remove functors+    by essentially inlining them.  To achieve this with just interfaces+    we'd have to store here the entire module, not just its interface.+    At the moment we work around this by passing all loaded modules to the+    type checker, so it looks up functors there, instead of in the interfaces,+    but we'd need to change this if we want better support for separate+    compilation. -}+   } deriving (Show, Generic, NFData)  filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls@@ -121,6 +121,8 @@   , ifAbstractTypes = filterMap (ifAbstractTypes ifs)   , ifDecls         = filterMap (ifDecls ifs)   , ifModules       = filterMap (ifModules ifs)+  , ifFunctors      = filterMap (ifFunctors ifs)+  , ifSignatures    = filterMap (ifSignatures ifs)   }   where   filterMap :: Map.Map Name a -> Map.Map Name a@@ -132,6 +134,8 @@                                , Map.keysSet (ifAbstractTypes i)                                , Map.keysSet (ifDecls i)                                , Map.keysSet (ifModules i)+                               , Map.keysSet (ifFunctors i)+                               , Map.keysSet (ifSignatures i)                                ]  @@ -142,30 +146,35 @@     , ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r)     , ifDecls    = Map.union (ifDecls l)    (ifDecls r)     , ifModules  = Map.union (ifModules l)  (ifModules r)+    , ifFunctors = Map.union (ifFunctors l) (ifFunctors r)+    , ifSignatures = ifSignatures l <> ifSignatures r     }  instance Monoid IfaceDecls where-  mempty      = IfaceDecls Map.empty Map.empty Map.empty Map.empty Map.empty-  mappend     = (<>)+  mempty      = IfaceDecls+                  { ifTySyns = mempty+                  , ifNewtypes = mempty+                  , ifAbstractTypes = mempty+                  , ifDecls = mempty+                  , ifModules = mempty+                  , ifFunctors = mempty+                  , ifSignatures = mempty+                  }+  mappend = (<>)   mconcat ds  = IfaceDecls     { ifTySyns   = Map.unions (map ifTySyns   ds)     , ifNewtypes = Map.unions (map ifNewtypes ds)     , ifAbstractTypes = Map.unions (map ifAbstractTypes ds)     , ifDecls    = Map.unions (map ifDecls    ds)     , ifModules  = Map.unions (map ifModules ds)+    , ifFunctors = Map.unions (map ifFunctors ds)+    , ifSignatures = Map.unions (map ifSignatures ds)     } -type IfaceTySyn = TySyn--ifTySynName :: TySyn -> Name-ifTySynName = tsName--type IfaceNewtype = Newtype-type IfaceAbstractType = AbstractType- data IfaceDecl = IfaceDecl   { ifDeclName    :: !Name          -- ^ Name of thing   , ifDeclSig     :: Schema         -- ^ Type+  , ifDeclIsPrim   :: !Bool   , ifDeclPragmas :: [Pragma]       -- ^ Pragmas   , ifDeclInfix   :: Bool           -- ^ Is this an infix thing   , ifDeclFixity  :: Maybe Fixity   -- ^ Fixity information@@ -176,15 +185,12 @@ -- | Produce a PrimMap from an interface. -- -- NOTE: the map will expose /both/ public and private names.+-- NOTE: this is a bit misnamed, as it is used to resolve known names+-- that Cryptol introduces (e.g., during type checking).  These+-- names need not be primitives.   A better way to do this in the future+-- might be to use original names instead (see #1522). ifacePrimMap :: Iface -> PrimMap-ifacePrimMap Iface { .. } =-  PrimMap { primDecls = merge primDecls-          , primTypes = merge primTypes }-  where-  merge f = Map.union (f public) (f private)--  public  = ifaceDeclsPrimMap ifPublic-  private = ifaceDeclsPrimMap ifPrivate+ifacePrimMap = ifaceDeclsPrimMap . ifDefines  ifaceDeclsPrimMap :: IfaceDecls -> PrimMap ifaceDeclsPrimMap IfaceDecls { .. } =@@ -199,6 +205,36 @@                           [ "Top level name not declared in a module?"                           , show n ] -  exprs    = map entry (Map.keys ifDecls)   newtypes = map entry (Map.keys ifNewtypes)+  exprs    = map entry (Map.keys ifDecls)   types    = map entry (Map.keys ifTySyns)+++-- | Given an interface computing a map from original names to actual names,+-- grouped by namespace.+ifaceOrigNameMap :: IfaceG name -> Map Namespace (Map OrigName Name)+ifaceOrigNameMap ifa = Map.unionsWith Map.union (here : nested)+  where+  here        = Map.fromList $+                  [ (NSValue, toMap vaNames) | not (Set.null vaNames) ] +++                  [ (NSType,  toMap tyNames) | not (Set.null tyNames) ] +++                  [ (NSValue, toMap moNames) | not (Set.null moNames) ]++  nested      = map ifaceOrigNameMap (Map.elems (ifFunctors decls))++  toMap names = Map.fromList+                  [ (og,x) | x <- Set.toList names, Just og <- [ asOrigName x ] ]++  decls       = ifDefines ifa+  from f      = Map.keysSet (f decls)+  tyNames     = Set.unions [ from ifTySyns, from ifNewtypes, from ifAbstractTypes ]+  moNames     = Set.unions [ from ifModules, from ifSignatures, from ifFunctors ]+  vaNames     = Set.unions [ newtypeCons, from ifDecls ]+  newtypeCons = Set.fromList (map ntConName (Map.elems (ifNewtypes decls)))+++++++

@@ -10,29 +10,33 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE BlockArguments #-} module Cryptol.ModuleSystem.Monad where  import           Cryptol.Eval (EvalEnv,EvalOpts(..)) +import           Cryptol.Backend.FFI (ForeignSrc)+import           Cryptol.Backend.FFI.Error import qualified Cryptol.Backend.Monad           as E  import           Cryptol.ModuleSystem.Env-import           Cryptol.ModuleSystem.Fingerprint+import qualified Cryptol.ModuleSystem.Env as MEnv import           Cryptol.ModuleSystem.Interface import           Cryptol.ModuleSystem.Name (FreshM(..),Supply) import           Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) import           Cryptol.ModuleSystem.NamingEnv(NamingEnv) import qualified Cryptol.Parser     as Parser import qualified Cryptol.Parser.AST as P-import           Cryptol.Parser.Position (Located) import           Cryptol.Utils.Panic (panic) import qualified Cryptol.Parser.NoPat as NoPat+import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards import qualified Cryptol.Parser.NoInclude as NoInc import qualified Cryptol.TypeCheck as T import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.Solver.SMT as SMT -import           Cryptol.Parser.Position (Range)+import           Cryptol.Parser.Position (Range, Located) import           Cryptol.Utils.Ident (interactiveName, noModuleName) import           Cryptol.Utils.PP import           Cryptol.Utils.Logger(Logger)@@ -42,9 +46,10 @@ import Control.Exception (IOException) import Data.ByteString (ByteString) import Data.Function (on)+import Data.Functor.Identity import Data.Map (Map)-import Data.Maybe (isJust) import Data.Text.Encoding.Error (UnicodeException)+import Data.Traversable import MonadLib import System.Directory (canonicalizePath) @@ -60,6 +65,7 @@ data ImportSource   = FromModule P.ModName   | FromImport (Located P.Import)+  | FromSigImport (Located P.ModName)   | FromModuleInstance (Located P.ModName)     deriving (Show, Generic, NFData) @@ -70,6 +76,7 @@   ppPrec _ is = case is of     FromModule n  -> text "module name" <+> pp n     FromImport li -> text "import of module" <+> pp (P.iModule (P.thing li))+    FromSigImport l -> text "import of interface" <+> pp (P.thing l)     FromModuleInstance l ->       text "instantiation of module" <+> pp (P.thing l) @@ -79,6 +86,7 @@     FromModule n          -> n     FromImport li         -> P.iModule (P.thing li)     FromModuleInstance l  -> P.thing l+    FromSigImport l       -> P.thing l   data ModuleError@@ -98,6 +106,8 @@     -- ^ Problems during the renaming phase   | NoPatErrors ImportSource [NoPat.Error]     -- ^ Problems during the NoPat phase+  | ExpandPropGuardsError ImportSource ExpandPropGuards.Error+    -- ^ Problems during the ExpandPropGuards phase   | NoIncludeErrors ImportSource [NoInc.IncludeError]     -- ^ Problems during the NoInclude phase   | TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)]@@ -108,11 +118,8 @@     -- ^ Module loaded by 'import' statement has the wrong module name   | DuplicateModuleName P.ModName FilePath FilePath     -- ^ Two modules loaded from different files have the same module name-  | ImportedParamModule P.ModName-    -- ^ Attempt to import a parametrized module that was not instantiated.-  | FailedToParameterizeModDefs P.ModName [T.Name]-    -- ^ Failed to add the module parameters to all definitions in a module.-  | NotAParameterizedModule P.ModName+  | FFILoadErrors P.ModName [FFILoadError]+    -- ^ Errors loading foreign function implementations    | ErrorInFile ModulePath ModuleError     -- ^ This is just a tag on the error, indicating the file containing it.@@ -131,6 +138,7 @@     RecursiveModules mods                -> mods `deepseq` ()     RenamerErrors src errs               -> src `deepseq` errs `deepseq` ()     NoPatErrors src errs                 -> src `deepseq` errs `deepseq` ()+    ExpandPropGuardsError src err        -> src `deepseq` err `deepseq` ()     NoIncludeErrors src errs             -> src `deepseq` errs `deepseq` ()     TypeCheckingFailed nm src errs       -> nm `deepseq` src `deepseq` errs `deepseq` ()     ModuleNameMismatch expected found    ->@@ -138,9 +146,7 @@     DuplicateModuleName name path1 path2 ->       name `deepseq` path1 `deepseq` path2 `deepseq` ()     OtherFailure x                       -> x `deepseq` ()-    ImportedParamModule x                -> x `deepseq` ()-    FailedToParameterizeModDefs x xs     -> x `deepseq` xs `deepseq` ()-    NotAParameterizedModule x            -> x `deepseq` ()+    FFILoadErrors x errs                 -> x `deepseq` errs `deepseq` ()     ErrorInFile x y                      -> x `deepseq` y `deepseq` ()  instance PP ModuleError where@@ -178,6 +184,8 @@      NoPatErrors _src errs -> vcat (map pp errs) +    ExpandPropGuardsError _src err -> pp err+     NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs)      TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs)@@ -185,7 +193,7 @@     ModuleNameMismatch expected found ->       hang (text "[error]" <+> pp (P.srcRange found) <.> char ':')          4 (vcat [ text "File name does not match module name:"-                 , text "Saw:"      <+> pp (P.thing found)+                 , text "  Actual:" <+> pp (P.thing found)                  , text "Expected:" <+> pp expected                  ]) @@ -196,16 +204,10 @@      OtherFailure x -> text x -    ImportedParamModule p ->-      text "[error] Import of a non-instantiated parameterized module:" <+> pp p--    FailedToParameterizeModDefs x xs ->-      hang (text "[error] Parameterized module" <+> pp x <+>-            text "has polymorphic parameters:")-         4 (commaSep (map pp xs))--    NotAParameterizedModule x ->-      text "[error] Module" <+> pp x <+> text "does not have parameters."+    FFILoadErrors x errs ->+      hang (text "[error] Failed to load foreign implementations for module"+            <+> pp x <.> colon)+         4 (vcat $ map pp errs)      ErrorInFile _ x -> ppPrec prec x @@ -238,6 +240,11 @@   src <- getImportSource   ModuleT (raise (NoPatErrors src errs)) +expandPropGuardsError :: ExpandPropGuards.Error -> ModuleM a+expandPropGuardsError err = do+  src <- getImportSource+  ModuleT (raise (ExpandPropGuardsError src err))+ noIncludeErrors :: [NoInc.IncludeError] -> ModuleM a noIncludeErrors errs = do   src <- getImportSource@@ -256,15 +263,8 @@ duplicateModuleName name path1 path2 =   ModuleT (raise (DuplicateModuleName name path1 path2)) -importParamModule :: P.ModName -> ModuleM a-importParamModule x = ModuleT (raise (ImportedParamModule x))--failedToParameterizeModDefs :: P.ModName -> [T.Name] -> ModuleM a-failedToParameterizeModDefs x xs =-  ModuleT (raise (FailedToParameterizeModDefs x xs))--notAParameterizedModule :: P.ModName -> ModuleM a-notAParameterizedModule x = ModuleT (raise (NotAParameterizedModule x))+ffiLoadErrors :: P.ModName -> [FFILoadError] -> ModuleM a+ffiLoadErrors x errs = ModuleT (raise (FFILoadErrors x errs))  -- | Run the computation, and if it caused and error, tag the error -- with the given file.@@ -423,13 +423,17 @@   env <- get   set $! f env -getLoadedMaybe :: P.ModName -> ModuleM (Maybe LoadedModule)+getLoadedMaybe :: P.ModName -> ModuleM (Maybe (LoadedModuleG T.TCTopEntity)) getLoadedMaybe mn = ModuleT $   do env <- get-     return (lookupModule mn env)+     return (lookupTCEntity mn env) +-- | This checks if the given name is loaded---it might refer to either+-- a module or a signature. isLoaded :: P.ModName -> ModuleM Bool-isLoaded mn = isJust <$> getLoadedMaybe mn+isLoaded mn =+  do env <- ModuleT get+     pure (MEnv.isLoaded mn (meLoadedModules env))  loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport  = loading . FromImport@@ -448,12 +452,12 @@ loading :: ImportSource -> ModuleM a -> ModuleM a loading src m = ModuleT $ do   ro <- ask-  let ro'  = ro { roLoading = src : roLoading ro }+  let new = src : roLoading ro    -- check for recursive modules-  when (src `elem` roLoading ro) (raise (RecursiveModules (roLoading ro')))+  when (src `elem` roLoading ro) (raise (RecursiveModules new)) -  local ro' (unModuleT m)+  local ro { roLoading = new } (unModuleT m)  -- | Get the currently focused import source. getImportSource :: ModuleM ImportSource@@ -463,17 +467,17 @@     is : _ -> return is     _      -> return (FromModule noModuleName) -getIface :: P.ModName -> ModuleM Iface-getIface mn = ($ mn) <$> getIfaces--getIfaces :: ModuleM (P.ModName -> Iface)-getIfaces = doLookup <$> ModuleT get+getIfaces :: ModuleM (Map P.ModName (Either T.ModParamNames Iface))+getIfaces = toMap <$> ModuleT get   where-  doLookup env mn =-    case lookupModule mn env of-      Just lm -> lmInterface lm-      Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]+  toMap env = cvt <$> getLoadedEntities (meLoadedModules env) +  cvt ent =+    case ent of+      ALoadedInterface ifa -> Left (lmData ifa)+      ALoadedFunctor mo -> Right (lmdInterface (lmData mo))+      ALoadedModule mo -> Right (lmdInterface (lmData mo))+ getLoaded :: P.ModName -> ModuleM T.Module getLoaded mn = ModuleT $   do env <- get@@ -481,6 +485,20 @@        Just lm -> return (lmModule lm)        Nothing -> panic "ModuleSystem" ["Module not available", show (pp mn) ] +getAllLoaded :: ModuleM (P.ModName -> Maybe (T.ModuleG (), IfaceG ()))+getAllLoaded = ModuleT+  do env <- get+     pure \nm -> do lm <- lookupModule nm env+                    pure ( (lmModule lm) { T.mName = () }+                         , ifaceForgetName (lmInterface lm)+                         )++getAllLoadedSignatures :: ModuleM (P.ModName -> Maybe T.ModParamNames)+getAllLoadedSignatures = ModuleT+  do env <- get+     pure \nm -> lmData <$> lookupSignature nm env++ getNameSeeds :: ModuleM T.NameSeeds getNameSeeds  = ModuleT (meNameSeeds `fmap` get) @@ -505,28 +523,42 @@   do env <- get      set $! env { meSupply = supply } -unloadModule :: (LoadedModule -> Bool) -> ModuleM ()+unloadModule :: (forall a. LoadedModuleG a -> Bool) -> ModuleM () unloadModule rm = ModuleT $ do   env <- get   set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }  loadedModule ::-  ModulePath -> Fingerprint -> NamingEnv -> T.Module -> ModuleM ()-loadedModule path fp nameEnv m = ModuleT $ do+  ModulePath ->+  FileInfo ->+  NamingEnv ->+  Maybe ForeignSrc ->+  T.TCTopEntity ->+  ModuleM ()+loadedModule path fi nameEnv fsrc m = ModuleT $ do   env <- get   ident <- case path of              InFile p  -> unModuleT $ io (canonicalizePath p)              InMem l _ -> pure l -  set $! env { meLoadedModules = addLoadedModule path ident fp nameEnv m-                                                        (meLoadedModules env) }+  let newLM =+        case m of+          T.TCTopModule mo -> addLoadedModule path ident fi nameEnv fsrc mo+          T.TCTopSignature x s -> addLoadedSignature path ident fi nameEnv x s -modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()-modifyEvalEnv f = ModuleT $ do+  set $! env { meLoadedModules = newLM (meLoadedModules env) }+++modifyEvalEnvM :: Traversable t =>+  (EvalEnv -> E.Eval (t EvalEnv)) -> ModuleM (t ())+modifyEvalEnvM f = ModuleT $ do   env <- get   let evalEnv = meEvalEnv env-  evalEnv' <- inBase $ E.runEval mempty (f evalEnv)-  set $! env { meEvalEnv = evalEnv' }+  tenv <- inBase (E.runEval mempty (f evalEnv))+  traverse (\evalEnv' -> set $! env { meEvalEnv = evalEnv' }) tenv++modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()+modifyEvalEnv = fmap runIdentity . modifyEvalEnvM . (fmap Identity .)  getEvalEnv :: ModuleM EvalEnv getEvalEnv  = ModuleT (meEvalEnv `fmap` get)

@@ -6,16 +6,15 @@ -- Stability   :  provisional -- Portability :  portable -{-# LANGUAGE Trustworthy #-}- {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE RankNTypes #-} -- for the instances of RunM and BaseM {-# LANGUAGE UndecidableInstances #-} @@ -25,12 +24,17 @@   , NameSource(..)   , nameUnique   , nameIdent+  , mapNameIdent   , nameInfo   , nameLoc   , nameFixity   , nameNamespace   , asPrim   , asOrigName+  , nameModPath+  , nameModPathMaybe+  , nameTopModule+  , nameTopModuleMaybe   , ppLocName   , Namespace(..)   , ModPath(..)@@ -38,15 +42,15 @@      -- ** Creation   , mkDeclared-  , mkParameter-  , toParamInstName-  , asParamName-  , paramModRecParam+  , mkLocal+  , asLocal+  , mkModParam      -- ** Unique Supply   , FreshM(..), nextUniqueM-  , SupplyT(), runSupplyT+  , SupplyT(), runSupplyT, runSupply   , Supply(), emptySupply, nextUnique+  , freshNameFor      -- ** PrimMap   , PrimMap(..)@@ -57,6 +61,7 @@ import           Control.DeepSeq import qualified Data.Map as Map import qualified Data.Monoid as M+import           Data.Functor.Identity(runIdentity) import           GHC.Generics (Generic) import           MonadLib import           Prelude ()@@ -66,36 +71,24 @@   -import           Cryptol.Parser.Position (Range,Located(..),emptyRange)+import           Cryptol.Parser.Position (Range,Located(..)) import           Cryptol.Utils.Fixity import           Cryptol.Utils.Ident import           Cryptol.Utils.Panic import           Cryptol.Utils.PP -+data NameInfo = GlobalName NameSource OrigName+              | LocalName Namespace Ident+                deriving (Generic, NFData, Show)  -- Names -------------------------------------------------------------------------- | Information about the binding site of the name.-data NameInfo = Declared !ModPath !NameSource-                -- ^ This name refers to a declaration from this module-              | Parameter-                -- ^ This name is a parameter (function or type)-                deriving (Eq, Show, Generic, NFData)-- data Name = Name { nUnique :: {-# UNPACK #-} !Int                    -- ^ INVARIANT: this field uniquely identifies a name for one                    -- session with the Cryptol library. Names are unique to                    -- their binding site.                   , nInfo :: !NameInfo-                   -- ^ Information about the origin of this name. -                 , nNamespace :: !Namespace--                 , nIdent :: !Ident-                   -- ^ The name of the identifier-                  , nFixity :: !(Maybe Fixity)                    -- ^ The associativity and precedence level of                    --   infix operators.  'Nothing' indicates an@@ -150,7 +143,12 @@   fmtPref og = case getNameFormat og disp of                  UnQualified -> ""                  Qualified q -> modNameToText q-                 NotInScope  -> Text.pack $ show $ pp (ogModule og)+                 NotInScope  ->+                    let m = Text.pack (show (pp (ogModule og)))+                    in+                    case ogSource og of+                      FromModParam q  -> m <> "::" <> Text.pack (show (pp q))+                      _ -> m    -- Note that this assumes that `xs` is `l` and `ys` is `r`   cmpText xs ys =@@ -173,10 +171,13 @@ -- the need for parentheses. ppName :: Name -> Doc ppName nm =-  case asOrigName nm of-    Just og -> pp og-    Nothing -> pp (nameIdent nm)-+  case nInfo nm of+    GlobalName _ og -> pp og+    LocalName _ i   -> pp i+  <.>+  withPPCfg \cfg ->+    if ppcfgShowNameUniques cfg then "_" <.> int (nameUnique nm)+                                else mempty  instance PP Name where   ppPrec _ = ppPrefixName@@ -184,12 +185,12 @@ instance PPName Name where   ppNameFixity n = nameFixity n -  ppInfixName n@Name { .. }-    | isInfixIdent nIdent = ppName n+  ppInfixName n+    | isInfixIdent (nameIdent n) = ppName n     | otherwise           = panic "Name" [ "Non-infix name used infix"-                                         , show nIdent ]+                                         , show (nameIdent n) ] -  ppPrefixName n@Name { .. } = optParens (isInfixIdent nIdent) (ppName n)+  ppPrefixName n = optParens (isInfixIdent (nameIdent n)) (ppName n)   -- | Pretty-print a name with its source location information.@@ -199,14 +200,26 @@ nameUnique :: Name -> Int nameUnique  = nUnique +nameInfo :: Name -> NameInfo+nameInfo = nInfo+ nameIdent :: Name -> Ident-nameIdent  = nIdent+nameIdent n = case nInfo n of+                GlobalName _ og -> ogName og+                LocalName _ i   -> i -nameNamespace :: Name -> Namespace-nameNamespace = nNamespace+mapNameIdent :: (Ident -> Ident) -> Name -> Name+mapNameIdent f n =+  n { nInfo =+        case nInfo n of+          GlobalName x og -> GlobalName x og { ogName = f (ogName og) }+          LocalName x i   -> LocalName x (f i)+    } -nameInfo :: Name -> NameInfo-nameInfo  = nInfo+nameNamespace :: Name -> Namespace+nameNamespace n = case nInfo n of+                    GlobalName _ og -> ogNamespace og+                    LocalName ns _  -> ns  nameLoc :: Name -> Range nameLoc  = nLoc@@ -216,31 +229,43 @@  -- | Primtiives must be in a top level module, at least for now. asPrim :: Name -> Maybe PrimIdent-asPrim Name { .. } =-  case nInfo of-    Declared (TopModule m) _ -> Just $ PrimIdent m $ identText nIdent-    _                        -> Nothing--toParamInstName :: Name -> Name-toParamInstName n =+asPrim n =   case nInfo n of-    Declared m s -> n { nInfo = Declared (apPathRoot paramInstModName m) s }-    Parameter   -> n+    GlobalName _ og+      | TopModule m <- ogModule og, not (ogFromModParam og) ->+        Just $ PrimIdent m $ identText $ ogName og -asParamName :: Name -> Name-asParamName n = n { nInfo = Parameter }+    _ -> Nothing  asOrigName :: Name -> Maybe OrigName-asOrigName nm =-  case nInfo nm of-    Declared p _ ->-      Just OrigName { ogModule    = apPathRoot notParamInstModName  p-                    , ogNamespace = nNamespace nm-                    , ogName      = nIdent nm-                    }-    Parameter    -> Nothing+asOrigName n =+  case nInfo n of+    GlobalName _ og -> Just og+    LocalName {}    -> Nothing +-- | Get the module path for the given name.+nameModPathMaybe :: Name -> Maybe ModPath+nameModPathMaybe n = ogModule <$> asOrigName n +-- | Get the module path for the given name.+-- The name should be a top-level name.+nameModPath :: Name -> ModPath+nameModPath n =+  case nameModPathMaybe n of+    Just p  -> p+    Nothing -> panic "nameModPath" [ "Not a top-level name: ", show n ]+++-- | Get the name of the top-level module that introduced this name.+nameTopModuleMaybe :: Name -> Maybe ModName+nameTopModuleMaybe = fmap topModuleFor . nameModPathMaybe++-- | Get the name of the top-level module that introduced this name.+-- Works only for top-level names (i.e., that have original names)+nameTopModule :: Name -> ModName+nameTopModule = topModuleFor . nameModPath++ -- Name Supply -----------------------------------------------------------------  class Monad m => FreshM m where@@ -271,6 +296,9 @@ runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a,Supply) runSupplyT s (SupplyT m) = runStateT s m +runSupply :: Supply -> (forall m. FreshM m => m a) -> (a,Supply)+runSupply s m = runIdentity (runSupplyT s m)+ instance Monad m => Functor (SupplyT m) where   fmap f (SupplyT m) = SupplyT (fmap f m)   {-# INLINE fmap #-}@@ -315,8 +343,8 @@ emptySupply :: Supply emptySupply  = Supply 0x1000 -- For one such name, see paramModRecParam--- XXX: perhaps we should simply not have such things, but that's the way--- for now.+-- XXX: perhaps we should simply not have such things+-- XXX: do we have these anymore?  nextUnique :: Supply -> (Int,Supply) nextUnique (Supply n) = s' `seq` (n,s')@@ -330,26 +358,77 @@ mkDeclared ::   Namespace -> ModPath -> NameSource -> Ident -> Maybe Fixity -> Range ->   Supply -> (Name,Supply)-mkDeclared nNamespace m sys nIdent nFixity nLoc s =-  let (nUnique,s') = nextUnique s-      nInfo        = Declared m sys-   in (Name { .. }, s')+mkDeclared ns m sys ident fixity loc s = (name, s')+  where+  (u,s') = nextUnique s+  name = Name { nUnique   = u+              , nFixity   = fixity+              , nLoc      = loc+              , nInfo     = GlobalName+                              sys+                              OrigName+                                { ogNamespace = ns+                                , ogModule    = m+                                , ogName      = ident+                                , ogSource    = FromDefinition+                                }+              }  -- | Make a new parameter name.-mkParameter :: Namespace -> Ident -> Range -> Supply -> (Name,Supply)-mkParameter nNamespace nIdent nLoc s =-  let (nUnique,s') = nextUnique s-      nFixity      = Nothing-   in (Name { nInfo = Parameter, .. }, s')+mkLocal :: Namespace -> Ident -> Range -> Supply -> (Name,Supply)+mkLocal ns ident loc s = (name, s')+  where+  (u,s')  = nextUnique s+  name    = Name { nUnique = u+                 , nLoc    = loc+                 , nFixity = Nothing+                 , nInfo   = LocalName ns ident+                 } -paramModRecParam :: Name-paramModRecParam = Name { nInfo = Parameter-                        , nFixity = Nothing-                        , nIdent  = packIdent "$modParams"-                        , nLoc    = emptyRange-                        , nUnique = 0x01-                        , nNamespace = NSValue-                        }+{- | Make a local name derived from the given name.+This is a bit questionable,+but it is used by the translation to SAW Core -}+asLocal :: Namespace -> Name -> Name+asLocal ns x =+  case nameInfo x of+    GlobalName _ og -> x { nInfo = LocalName ns (ogName og) }+    LocalName {}    -> x++mkModParam ::+  ModPath {- ^ Module containing the parameter -} ->+  Ident   {- ^ Name of the module parameter    -} ->+  Range   {- ^ Location                        -} ->+  Name    {- ^ Name in the signature           -} ->+  Supply -> (Name, Supply)+mkModParam own pname rng n s = (name, s')+  where+  (u,s') = nextUnique s+  name = Name { nUnique = u+              , nInfo   = GlobalName+                            UserName+                            OrigName+                              { ogModule    = own+                              , ogName      = nameIdent n+                              , ogNamespace = nameNamespace n+                              , ogSource    = FromModParam pname+                              }+              , nFixity = nFixity n+              , nLoc    = rng+              }++-- | This is used when instantiating functors+freshNameFor :: ModPath -> Name -> Supply -> (Name,Supply)+freshNameFor mpath x s = (newName, s1)+  where+  (u,s1) = nextUnique s+  newName =+    x { nUnique = u+      , nInfo =+          case nInfo x of+            GlobalName src og -> GlobalName src og { ogModule = mpath+                                                   , ogSource = FromFunctorInst }+            LocalName {} -> panic "freshNameFor" ["Unexpected local",show x]+      }  -- Prim Maps ------------------------------------------------------------------- 

@@ -0,0 +1,88 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE BlockArguments #-}+module Cryptol.ModuleSystem.Names where++import Data.Set(Set)+import qualified Data.Set as Set+import Control.DeepSeq(NFData)+import GHC.Generics (Generic)++import Cryptol.Utils.Panic (panic)+import Cryptol.ModuleSystem.Name+++-- | A non-empty collection of names used by the renamer.+data Names = One Name | Ambig (Set Name) -- ^ Non-empty+  deriving (Show,Generic,NFData)++namesToList :: Names -> [Name]+namesToList xs =+  case xs of+    One x -> [x]+    Ambig ns -> Set.toList ns++anyOne :: Names -> Name+anyOne = head . namesToList++instance Semigroup Names where+  xs <> ys =+    case (xs,ys) of+      (One x, One y)+        | x == y           -> One x+        | otherwise        -> Ambig $! Set.fromList [x,y]+      (One x, Ambig as)    -> Ambig $! Set.insert x as+      (Ambig as, One x)    -> Ambig $! Set.insert x as+      (Ambig as, Ambig bs) -> Ambig $! Set.union as bs++namesFromSet :: Set Name {- ^ Non-empty -} -> Names+namesFromSet xs =+  case Set.minView xs of+    Just (a,ys) -> if Set.null ys then One a else Ambig xs+    Nothing     -> panic "namesFromSet" ["empty set"]++unionManyNames :: [Names] -> Maybe Names+unionManyNames xs =+  case xs of+    [] -> Nothing+    _  -> Just (foldr1 (<>) xs)++mapNames :: (Name -> Name) -> Names -> Names+mapNames f xs =+  case xs of+    One x -> One (f x)+    Ambig as -> namesFromSet (Set.map f as)++filterNames :: (Name -> Bool) -> Names -> Maybe Names+filterNames p names =+  case names of+    One x -> if p x then Just (One x) else Nothing+    Ambig xs -> do let ys = Set.filter p xs+                   (y,zs) <- Set.minView ys+                   if Set.null zs then Just (One y) else Just (Ambig ys)++travNames :: Applicative f => (Name -> f Name) -> Names -> f Names+travNames f xs =+  case xs of+    One x -> One <$> f x+    Ambig as -> namesFromSet . Set.fromList <$> traverse f (Set.toList as)+++-- Names that are in the first but not the second+diffNames :: Names -> Names -> Maybe Names+diffNames x y =+  case x of+    One a ->+      case y of+        One b -> if a == b then Nothing+                           else Just (One a)+        Ambig xs -> if a `Set.member` xs then Nothing else Just (One a)+    Ambig xs ->+      do (a,rest) <- Set.minView ys+         pure if Set.null rest then One a else Ambig xs++      where+      ys = case y of+             One z    -> Set.delete z xs+             Ambig zs -> Set.difference xs zs+

@@ -7,112 +7,119 @@ -- Portability :  portable  {-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveTraversable #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE RecordWildCards #-} {-# 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 -import Data.List (nub)-import Data.Maybe (fromMaybe,mapMaybe,maybeToList)+import Data.Maybe (mapMaybe,maybeToList) import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import           Data.Set (Set) import qualified Data.Set as Set-import Data.Semigroup-import MonadLib (runId,Id,StateT,runStateT,lift,sets_,forM_)+import           Data.Foldable(foldl')  import GHC.Generics (Generic)-import Control.DeepSeq--import Prelude ()-import Prelude.Compat+import Control.DeepSeq(NFData)  import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.Ident(allNamespaces) import Cryptol.Parser.AST-import Cryptol.Parser.Name(isGeneratedName)-import Cryptol.Parser.Position import qualified Cryptol.TypeCheck.AST as T-import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name+import Cryptol.ModuleSystem.Names+import Cryptol.ModuleSystem.Interface  --- Naming Environment ----------------------------------------------------------- -- | The 'NamingEnv' is used by the renamer to determine what -- identifiers refer to.-newtype NamingEnv = NamingEnv (Map Namespace (Map PName [Name]))+newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names))   deriving (Show,Generic,NFData) --- | All names mentioned in the environment-namingEnvNames :: NamingEnv -> Set Name-namingEnvNames (NamingEnv xs) =-  Set.fromList $ concatMap (concat . Map.elems) $ Map.elems xs+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) --- | Get the names in a given namespace-namespaceMap :: Namespace -> NamingEnv -> Map PName [Name]-namespaceMap ns (NamingEnv env) = Map.findWithDefault Map.empty ns env+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)) --- | Resolve a name in the given namespace.-lookupNS :: Namespace -> PName -> NamingEnv -> [Name]-lookupNS ns x = Map.findWithDefault [] x . namespaceMap ns --- | Return a list of value-level names to which this parsed name may refer.-lookupValNames :: PName -> NamingEnv -> [Name]-lookupValNames = lookupNS NSValue---- | Return a list of type-level names to which this parsed name may refer.-lookupTypeNames :: PName -> NamingEnv -> [Name]-lookupTypeNames = lookupNS NSType+{- | This "joins" two naming environments by matching the text name.+The result maps the unique names from the first environment with the+matching names in the second.  This is used to compute the naming for+an instantiated functor:+  * if the left environment has the defined names of the functor, and+  * the right one has the defined names of the instantiation, then+  * the result maps functor names to instance names.+-}+zipByTextName :: NamingEnv -> NamingEnv -> Map Name Name+zipByTextName (NamingEnv k) (NamingEnv v) = Map.fromList $ doInter doNS k v+  where+  doInter :: Ord k => (a -> b -> [c]) -> Map k a -> Map k b -> [c]+  doInter f a b = concat (Map.elems (Map.intersectionWith f a b)) --- | Singleton renaming environment for the given namespace.-singletonNS :: Namespace -> PName -> Name -> NamingEnv-singletonNS ns pn n = NamingEnv (Map.singleton ns (Map.singleton pn [n]))+  doNS :: Map PName Names -> Map PName Names -> [(Name,Name)]+  doNS as bs = doInter doPName as bs --- | Singleton expression renaming environment.-singletonE :: PName -> Name -> NamingEnv-singletonE = singletonNS NSValue+  doPName :: Names -> Names -> [(Name,Name)]+  doPName xs ys = [ (x,y) | x <- namesToList xs, y <- namesToList ys ]+  -- NOTE: we'd exepct that there are no ambiguities in the environments. --- | Singleton type renaming environment.-singletonT :: PName -> Name -> NamingEnv-singletonT = singletonNS NSType+-- | Keep only the bindings in the 1st environment that are *NOT* in the second.+without :: NamingEnv -> NamingEnv -> NamingEnv+NamingEnv keep `without` NamingEnv remove = NamingEnv result+  where+  result     = Map.differenceWith rmInNS keep remove+  rmInNS a b = let c = Map.differenceWith diffNames a b+               in if Map.null c then Nothing else Just c +-- | All names mentioned in the environment+namingEnvNames :: NamingEnv -> Set Name+namingEnvNames (NamingEnv xs) =+  case unionManyNames (mapMaybe (unionManyNames . Map.elems) (Map.elems xs)) of+    Nothing -> Set.empty+    Just (One x) -> Set.singleton x+    Just (Ambig as) -> as -namingEnvRename :: (Name -> Name) -> NamingEnv -> NamingEnv-namingEnvRename f (NamingEnv mp) = NamingEnv (ren <$> mp)+-- | Get a unqualified naming environment for the given names+namingEnvFromNames :: Set Name -> NamingEnv+namingEnvFromNames xs = NamingEnv (foldl' add mempty xs)   where-  ren nsm = map f <$> nsm+  add mp x = let ns = nameNamespace x+                 txt = nameIdent x+             in Map.insertWith (Map.unionWith (<>))+                               ns (Map.singleton (mkUnqual txt) (One x))+                               mp  -instance Semigroup NamingEnv where-  NamingEnv l <> NamingEnv r =-      NamingEnv (Map.unionWith (Map.unionWith merge) l r)--instance Monoid NamingEnv where-  mempty = NamingEnv Map.empty-  {-# INLINE mempty #-}+-- | Get the names in a given namespace+namespaceMap :: Namespace -> NamingEnv -> Map PName Names+namespaceMap ns (NamingEnv env) = Map.findWithDefault Map.empty ns env +-- | Resolve a name in the given namespace.+lookupNS :: Namespace -> PName -> NamingEnv -> Maybe Names+lookupNS ns x env = Map.lookup x (namespaceMap ns env) --- | Merge two name maps, collapsing cases where the entries are the same, and--- producing conflicts otherwise.-merge :: [Name] -> [Name] -> [Name]-merge xs ys | xs == ys  = xs-            | otherwise = nub (xs ++ ys)+-- | Resolve a name in the given namespace.+lookupListNS :: Namespace -> PName -> NamingEnv -> [Name]+lookupListNS ns x env =+  case lookupNS ns x env of+    Nothing -> []+    Just as -> namesToList as -instance PP NamingEnv where-  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps-    where ppNS (ns,xs) = pp ns $$ nest 2 (vcat (map ppNm (Map.toList xs)))-          ppNm (x,as)  = pp x <+> "->" <+> commaSep (map pp as)+-- | Singleton renaming environment for the given namespace.+singletonNS :: Namespace -> PName -> Name -> NamingEnv+singletonNS ns pn n = NamingEnv (Map.singleton ns (Map.singleton pn (One n)))  -- | Generate a mapping from 'PrimIdent' to 'Name' for a -- given naming environment.@@ -124,7 +131,8 @@     }   where   fromNS ns = Map.fromList-                [ entry x | xs <- Map.elems (namespaceMap ns env), x <- xs ]+                [ entry x | xs <- Map.elems (namespaceMap ns env)+                          , x <- namesToList xs ]    entry n = case asPrim n of               Just p  -> (p,n)@@ -139,9 +147,9 @@   where   names = Map.fromList             [ (og, qn)-              | ns            <- [ NSValue, NSType, NSModule ]+              | ns            <- allNamespaces               , (pn,xs)       <- Map.toList (namespaceMap ns env)-              , x             <- xs+              , x             <- namesToList xs               , og            <- maybeToList (asOrigName x)               , let qn = case getModName pn of                           Just q  -> Qualified q@@ -154,145 +162,127 @@ -- NOTE: if entries in the NamingEnv would have produced a name clash, -- they will be omitted from the resulting sets. visibleNames :: NamingEnv -> Map Namespace (Set Name)-visibleNames (NamingEnv env) = Set.fromList . mapMaybe check . Map.elems <$> env-  where-  check names =-    case names of-      [name] -> Just name-      _      -> Nothing+visibleNames (NamingEnv env) = check <$> env+  where check mp = Set.fromList [ a | One a <- Map.elems mp ]  -- | Qualify all symbols in a 'NamingEnv' with the given prefix. qualify :: ModName -> NamingEnv -> NamingEnv qualify pfx (NamingEnv env) = NamingEnv (Map.mapKeys toQual <$> env)   where-  -- XXX we don't currently qualify fresh names+  -- We don't qualify fresh names, because they should not be directly+  -- visible to the end users (i.e., they shouldn't really be exported)   toQual (Qual _ n)  = Qual pfx n   toQual (UnQual n)  = Qual pfx n   toQual n@NewName{} = n -filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv-filterNames p (NamingEnv env) = NamingEnv (Map.filterWithKey check <$> env)-  where check n _ = p n----- | Like mappend, but when merging, prefer values on the lhs.-shadowing :: NamingEnv -> NamingEnv -> NamingEnv-shadowing (NamingEnv l) (NamingEnv r) = NamingEnv (Map.unionWith Map.union l r)+filterPNames :: (PName -> Bool) -> NamingEnv -> NamingEnv+filterPNames p (NamingEnv env) = NamingEnv (Map.mapMaybe checkNS env)+  where+  checkNS nsMap = let new = Map.filterWithKey (\n _ -> p n) nsMap+                  in if Map.null new then Nothing else Just new -travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv-travNamingEnv f (NamingEnv mp) =-  NamingEnv <$> traverse (traverse (traverse f)) mp+filterUNames :: (Name -> Bool) -> NamingEnv -> NamingEnv+filterUNames p (NamingEnv env) = NamingEnv (Map.mapMaybe check env)+  where+  check nsMap = let new = Map.mapMaybe (filterNames p) nsMap+                in if Map.null new then Nothing else Just new  -{- | Do somethign in context.  If `Nothing` than we are working with-a local declaration. Otherwise we are at the top-level of the-given module. -}-data InModule a = InModule (Maybe ModPath) a-                  deriving (Functor,Traversable,Foldable,Show)-+-- | Find the ambiguous entries in an environmet.+-- A name is ambiguous if it might refer to multiple entities.+findAmbig :: NamingEnv -> [ [Name] ]+findAmbig (NamingEnv ns) =+  [ Set.toList xs+  | mp <- Map.elems ns+  , Ambig xs <- Map.elems mp+  ] -newTop ::-  FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name-newTop ns m thing fx rng =-  liftSupply (mkDeclared ns m src (getIdent thing) fx rng)-  where src = if isGeneratedName thing then SystemName else UserName+-- | Get the subset of the first environment that shadows something+-- in the second one.+findShadowing :: NamingEnv -> NamingEnv -> [ (PName,Name,[Name]) ]+findShadowing (NamingEnv lhs) rhs =+  [ (p, anyOne xs, namesToList ys)+  | (ns,mp) <- Map.toList lhs+  , (p,xs) <- Map.toList mp+  , Just ys <- [ lookupNS ns p rhs ]+  ] -newLocal :: FreshM m => Namespace -> PName -> Range -> m Name-newLocal ns thing rng = liftSupply (mkParameter ns (getIdent thing) rng)+-- | Do an arbitrary choice for ambiguous names.+-- We do this to continue checking afetr we've reported an ambiguity error.+forceUnambig :: NamingEnv -> NamingEnv+forceUnambig (NamingEnv mp) = NamingEnv (fmap (One . anyOne) <$> mp) -newtype BuildNamingEnv = BuildNamingEnv { runBuild :: SupplyT Id NamingEnv }+-- | Like mappend, but when merging, prefer values on the lhs.+shadowing :: NamingEnv -> NamingEnv -> NamingEnv+shadowing (NamingEnv l) (NamingEnv r) = NamingEnv (Map.unionWith Map.union l r) +mapNamingEnv :: (Name -> Name) -> NamingEnv -> NamingEnv+mapNamingEnv f (NamingEnv mp) = NamingEnv (fmap (mapNames f) <$> mp) -buildNamingEnv :: BuildNamingEnv -> Supply -> (NamingEnv,Supply)-buildNamingEnv b supply = runId $ runSupplyT supply $ runBuild b+travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv+travNamingEnv f (NamingEnv mp) =+  NamingEnv <$> traverse (traverse (travNames f)) mp --- | Generate a 'NamingEnv' using an explicit supply.-defsOf :: BindsNames a => a -> Supply -> (NamingEnv,Supply)-defsOf = buildNamingEnv . namingEnv+isEmptyNamingEnv :: NamingEnv -> Bool+isEmptyNamingEnv (NamingEnv mp) = Map.null mp+-- This assumes that we've been normalizing away empty maps, hopefully+-- we've been doing it everywhere.  ------------------------------------------------------------------------------------ Collect definitions of nested modules--type NestedMods = Map Name NamingEnv-type CollectM   = StateT NestedMods (SupplyT Id)--collectNestedModules ::-  NamingEnv -> Module PName -> Supply -> (NestedMods, Supply)-collectNestedModules env m =-  collectNestedModulesDecls env (thing (mName m)) (mDecls m)--collectNestedModulesDecls ::-  NamingEnv -> ModName -> [TopDecl PName] -> Supply -> (NestedMods, Supply)-collectNestedModulesDecls env m ds sup = (mp,newS)+-- | Compute an unqualified naming environment, containing the various module+-- parameters.+modParamsNamingEnv :: T.ModParamNames -> NamingEnv+modParamsNamingEnv T.ModParamNames { .. } =+  NamingEnv $ Map.fromList+    [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns)+    , (NSType,  Map.fromList $ map fromTS (Map.elems mpnTySyn) +++                               map fromTy (Map.elems mpnTypes))+    ]   where-  s0            = Map.empty-  mpath         = TopModule m-  ((_,mp),newS) = runId $ runSupplyT sup $ runStateT s0 $-                  collectNestedModulesDs mpath env ds--collectNestedModulesDs :: ModPath -> NamingEnv -> [TopDecl PName] -> CollectM ()-collectNestedModulesDs mpath env ds =-  forM_ [ tlValue nm | DModule nm <- ds ] \(NestedModule nested) ->-    do let pname = thing (mName nested)-           name  = case lookupNS NSModule pname env of-                     n : _ -> n -- if a name is ambiguous we may get-                                -- multiple answers, but we just pick one.-                                -- This should be OK, as the error should be-                                -- caught during actual renaming.-                     _   -> panic "collectedNestedModulesDs"-                             [ "Missing definition for " ++ show pname ]-       newEnv <- lift (runBuild (moduleDefs (Nested mpath (nameIdent name)) nested))-       sets_ (Map.insert name newEnv)-       let newMPath = Nested mpath (nameIdent name)-       collectNestedModulesDs newMPath newEnv (mDecls nested)+  toPName n = mkUnqual (nameIdent n) ---------------------------------------------------------------------------------+  fromTy tp = let nm = T.mtpName tp+              in (toPName nm, One nm) +  fromFu f  = (toPName f, One f) +  fromTS ts = (toPName (T.tsName ts), One (T.tsName ts))  -instance Semigroup BuildNamingEnv where-  BuildNamingEnv a <> BuildNamingEnv b = BuildNamingEnv $-    do x <- a-       y <- b-       return (mappend x y)--instance Monoid BuildNamingEnv where-  mempty = BuildNamingEnv (pure mempty)--  mappend = (<>)--  mconcat bs = BuildNamingEnv $-    do ns <- sequence (map runBuild bs)-       return (mconcat ns)-----------------------------------------------------------------------------------+-- | 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 ]+  where+  toPName n = mkUnqual (nameIdent n) +  exprs   = mconcat [ singletonNS NSValue (toPName n) n+                    | n <- Map.keys ifDecls ] --- | Things that define exported names.-class BindsNames a where-  namingEnv :: a -> BuildNamingEnv+  tySyns  = mconcat [ singletonNS NSType (toPName n) n+                    | n <- Map.keys ifTySyns ] -instance BindsNames NamingEnv where-  namingEnv env = BuildNamingEnv (return env)-  {-# INLINE namingEnv #-}+  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+                            ]+                    ] -instance BindsNames a => BindsNames (Maybe a) where-  namingEnv = foldMap namingEnv-  {-# INLINE namingEnv #-}+  absTys  = mconcat [ singletonNS NSType (toPName n) n+                    | n <- Map.keys ifAbstractTypes ] -instance BindsNames a => BindsNames [a] where-  namingEnv = foldMap namingEnv-  {-# INLINE namingEnv #-}+  ntExprs = mconcat [ singletonNS NSValue (toPName n) n+                    | n <- Map.keys ifNewtypes ] --- | Generate a type renaming environment from the parameters that are bound by--- this schema.-instance BindsNames (Schema PName) where-  namingEnv (Forall ps _ _ _) = foldMap namingEnv ps-  {-# INLINE namingEnv #-}+  mods    = mconcat [ singletonNS NSModule (toPName n) n+                    | n <- Map.keys ifModules ] +  sigs    = mconcat [ singletonNS NSModule (toPName n) n+                    | n <- Map.keys ifSignatures ]   -- | Adapt the things exported by something to the specific import/open.@@ -309,166 +299,12 @@   -- restrict or hide imported symbols   restricted     | Just (Hiding ns) <- iSpec imp =-       filterNames (\qn -> not (getIdent qn `elem` ns)) public+       filterPNames (\qn -> not (getIdent qn `elem` ns)) public      | Just (Only ns) <- iSpec imp =-       filterNames (\qn -> getIdent qn `elem` ns) public+       filterPNames (\qn -> getIdent qn `elem` ns) public      | otherwise = public   --- | Interpret an import in the context of an interface, to produce a name--- environment for the renamer, and a 'NameDisp' for pretty-printing.-interpImportIface :: Import     {- ^ The import declarations -} ->-                IfaceDecls {- ^ Declarations of imported module -} ->-                NamingEnv-interpImportIface imp = interpImportEnv imp . unqualifiedEnv----- | 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 ]-  where-  toPName n = mkUnqual (nameIdent n)--  exprs   = mconcat [ singletonE (toPName n) n | n <- Map.keys ifDecls ]-  tySyns  = mconcat [ singletonT (toPName n) n | n <- Map.keys ifTySyns ]-  ntTypes = mconcat [ singletonT (toPName n) n | n <- Map.keys ifNewtypes ]-  absTys  = mconcat [ singletonT (toPName n) n | n <- Map.keys ifAbstractTypes ]-  ntExprs = mconcat [ singletonE (toPName n) n | n <- Map.keys ifNewtypes ]-  mods    = mconcat [ singletonNS NSModule (toPName n) n-                                                | n <- Map.keys ifModules ]---- | Compute an unqualified naming environment, containing the various module--- parameters.-modParamsNamingEnv :: IfaceParams -> NamingEnv-modParamsNamingEnv IfaceParams { .. } =-  NamingEnv $ Map.fromList-    [ (NSValue, Map.fromList $ map fromFu $ Map.keys ifParamFuns)-    , (NSType,  Map.fromList $ map fromTy $ Map.elems ifParamTypes)-    ]-  where-  toPName n = mkUnqual (nameIdent n)--  fromTy tp = let nm = T.mtpName tp-              in (toPName nm, [nm])--  fromFu f  = (toPName f, [f])----data ImportIface = ImportIface Import Iface---- | Produce a naming environment from an interface file, that contains a--- mapping only from unqualified names to qualified ones.-instance BindsNames ImportIface where-  namingEnv (ImportIface imp Iface { .. }) = BuildNamingEnv $-    return (interpImportIface imp ifPublic)-  {-# INLINE namingEnv #-}---- | Introduce the name-instance BindsNames (InModule (Bind PName)) where-  namingEnv (InModule mb b) = BuildNamingEnv $-    do let Located { .. } = bName b-       n <- case mb of-              Just m  -> newTop NSValue m thing (bFixity b) srcRange-              Nothing -> newLocal NSValue thing srcRange -- local fixitiies?--       return (singletonE thing n)---- | Generate the naming environment for a type parameter.-instance BindsNames (TParam PName) where-  namingEnv TParam { .. } = BuildNamingEnv $-    do let range = fromMaybe emptyRange tpRange-       n <- newLocal NSType tpName range-       return (singletonT tpName n)---- | The naming environment for a single module.  This is the mapping from--- unqualified names to fully qualified names with uniques.-instance BindsNames (Module PName) where-  namingEnv m = moduleDefs (TopModule (thing (mName m))) m---moduleDefs :: ModPath -> ModuleG mname PName -> BuildNamingEnv-moduleDefs m Module { .. } = foldMap (namingEnv . InModule (Just m)) mDecls---instance BindsNames (InModule (TopDecl PName)) where-  namingEnv (InModule ns td) =-    case td of-      Decl d           -> namingEnv (InModule ns (tlValue d))-      DPrimType d      -> namingEnv (InModule ns (tlValue d))-      TDNewtype d      -> namingEnv (InModule ns (tlValue d))-      DParameterType d -> namingEnv (InModule ns d)-      DParameterConstraint {} -> mempty-      DParameterFun  d -> namingEnv (InModule ns d)-      Include _        -> mempty-      DImport {}       -> mempty -- see 'openLoop' in the renamer-      DModule m        -> namingEnv (InModule ns (tlValue m))---instance BindsNames (InModule (NestedModule PName)) where-  namingEnv (InModule ~(Just m) (NestedModule mdef)) = BuildNamingEnv $-    do let pnmame = mName mdef-       nm   <- newTop NSModule m (thing pnmame) Nothing (srcRange pnmame)-       pure (singletonNS NSModule (thing pnmame) nm)--instance BindsNames (InModule (PrimType PName)) where-  namingEnv (InModule ~(Just m) PrimType { .. }) =-    BuildNamingEnv $-      do let Located { .. } = primTName-         nm <- newTop NSType m thing primTFixity srcRange-         pure (singletonT thing nm)--instance BindsNames (InModule (ParameterFun PName)) where-  namingEnv (InModule ~(Just ns) ParameterFun { .. }) = BuildNamingEnv $-    do let Located { .. } = pfName-       ntName <- newTop NSValue ns thing pfFixity srcRange-       return (singletonE thing ntName)--instance BindsNames (InModule (ParameterType PName)) where-  namingEnv (InModule ~(Just ns) ParameterType { .. }) = BuildNamingEnv $-    -- XXX: we don't seem to have a fixity environment at the type level-    do let Located { .. } = ptName-       ntName <- newTop NSType ns thing Nothing srcRange-       return (singletonT thing ntName)---- NOTE: we use the same name at the type and expression level, as there's only--- ever one name introduced in the declaration. The names are only ever used in--- different namespaces, so there's no ambiguity.-instance BindsNames (InModule (Newtype PName)) where-  namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $-    do let Located { .. } = nName-       ntName <- newTop NSType ns thing Nothing srcRange-       -- XXX: the name reuse here is sketchy-       return (singletonT thing ntName `mappend` singletonE thing ntName)---- | The naming environment for a single declaration.-instance BindsNames (InModule (Decl PName)) where-  namingEnv (InModule pfx d) = case d of-    DBind b                 -> namingEnv (InModule pfx b)-    DSignature ns _sig      -> foldMap qualBind ns-    DPragma ns _p           -> foldMap qualBind ns-    DType syn               -> qualType (tsName syn) (tsFixity syn)-    DProp syn               -> qualType (psName syn) (psFixity syn)-    DLocated d' _           -> namingEnv (InModule pfx d')-    DRec {}                 -> panic "namingEnv" [ "DRec" ]-    DPatBind _pat _e        -> panic "namingEnv" ["Unexpected pattern binding"]-    DFixity{}               -> panic "namingEnv" ["Unexpected fixity declaration"]--    where--    mkName ns ln fx = case pfx of-                        Just m  -> newTop ns m (thing ln) fx (srcRange ln)-                        Nothing -> newLocal ns (thing ln) (srcRange ln)--    qualBind ln = BuildNamingEnv $-      do n <- mkName NSValue ln Nothing-         return (singletonE (thing ln) n)--    qualType ln f = BuildNamingEnv $-      do n <- mkName NSType ln f-         return (singletonT (thing ln) n)

@@ -10,9 +10,10 @@ {-# Language FlexibleInstances #-} {-# Language FlexibleContexts #-} {-# Language BlockArguments #-}+{-# Language OverloadedStrings #-} module Cryptol.ModuleSystem.Renamer (     NamingEnv(), shadowing-  , BindsNames(..), InModule(..)+  , BindsNames, InModule(..)   , shadowNames   , Rename(..), runRenamer, RenameM()   , RenamerError(..)@@ -30,154 +31,301 @@ import Prelude.Compat  import Data.Either(partitionEithers)-import Data.Maybe(fromJust)-import Data.List(find,foldl')+import Data.Maybe(mapMaybe)+import Data.List(find,groupBy,sortBy)+import Data.Function(on) import Data.Foldable(toList)-import Data.Map.Strict(Map)+import Data.Map(Map) import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Graph(SCC(..)) import Data.Graph.SCC(stronglyConnComp)-import           MonadLib hiding (mapM, mapM_)+import MonadLib hiding (mapM, mapM_)   import Cryptol.ModuleSystem.Name+import Cryptol.ModuleSystem.Names import Cryptol.ModuleSystem.NamingEnv import Cryptol.ModuleSystem.Exports-import Cryptol.Parser.Position(getLoc)+import Cryptol.Parser.Position(Range) import Cryptol.Parser.AST import Cryptol.Parser.Selector(selName) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.RecordMap-import Cryptol.Utils.Ident(allNamespaces,packModName)+import Cryptol.Utils.Ident(allNamespaces,OrigName(..),modPathCommon,+                              undefinedModName)+import Cryptol.Utils.PP  import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Renamer.Error+import Cryptol.ModuleSystem.Binds import Cryptol.ModuleSystem.Renamer.Monad+import Cryptol.ModuleSystem.Renamer.Imports+import Cryptol.ModuleSystem.Renamer.ImplicitImports  +{-+The Renamer Algorithm+=====================++1. Add implicit imports for visible nested modules++2. Compute what each module defines   (see "Cryptol.ModuleSystem.Binds")+  - This assigns unique names to names introduces by various declarations+  - Here we detect repeated top-level definitions in a module.+  - Module instantiations also get a name, but are not yet resolved, so+    we don't know what's defined by them.+  - We do not generate unique names for functor parameters---those will+    be matched textually to the arguments when applied.+  - We *do* generate unique names for declarations in "signatures"+    * those are only really needed when renaming the signature (step 4)+      (e.g., to determine if a name refers to something declared in the+      signature or something else).+    * when validating a module against a signature the names of the declarations+      are matched textually, *not* using the unique names+      (e.g., `x` in a signature is matched with the thing named `x` in a module,+       even though these two `x`s will have different unique `id`s)+++3. Resolve imports and instantiations (see "Cryptol.ModuleSystem.Imports")+  - Resolves names in submodule imports+  - Resolves functor instantiations:+    * generate new names for declarations in the functors.+    * this includes any nested modules, and things nested within them.+  - At this point we have enough information to know what's exported by+    each module.++4. Do the renaming (this module)+  - Using step 3 we compute the scoping environment for each module/signature+  - We traverse all declarations and replace the parser names with the+    corresponding names in scope:+    * Here we detect ambiguity and undefined errors+    * During this pass is also where we keep track of information of what+      names are used by declarations:+      - this is used to compute the dependencies between declarations+      - which are in turn used to order the declarations in dependency order+        * this is assumed by the TC+        * here we also report errors about invalid recursive dependencies+    * During this stage we also issue warning about unused type names+      (and we should probably do unused value names too one day)+  - During the rewriting we also do:+    - rebalance expression trees using the operator fixities+    - desugar record update notation+-}+++-- | The result of renaming a module 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+  , rmImported :: IfaceDecls+    -- ^ Imported declarations.  This provides the types for external+    -- names (used by the type-checker).   } +-- | Entry point. This is used for renaming a top-level module. renameModule :: Module PName -> RenameM RenamedModule renameModule m0 =-  do let m = m0 { mDecls = snd (addImplicitNestedImports (mDecls m0)) }-     env      <- liftSupply (defsOf m)-     nested   <- liftSupply (collectNestedModules env m)-     setNestedModule (nestedModuleNames nested)-       do (ifs,(inScope,m1)) <- collectIfaceDeps-                 $ renameModule' nested env (TopModule (thing (mName m))) m+  do -- Step 1: add implicit imports+     let m = m0 { mDef =+                    case mDef m0 of+                      NormalModule ds ->+                        NormalModule (addImplicitNestedImports ds)+                      FunctorInstance f as i -> FunctorInstance f as i+                      InterfaceModule s -> InterfaceModule s+                 }++     -- Step 2: compute what's defined+     (defs,errs) <- liftSupply (modBuilder (topModuleDefs m))+     mapM_ recordError errs++     -- Step 3: resolve imports+     extern       <- getExternal+     resolvedMods <- liftSupply (resolveImports extern defs)++     let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)+                                   | ImpNested x <- Map.keys resolvedMods ]+++     let mname = ImpTop (thing (mName m))++     setResolvedLocals resolvedMods $+       setNestedModule pathToName+       do (ifs,(inScope,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?+                  -- XXX: maybe we should keep the nested defines too?                  } +++++{- | Entry point. Rename a list of top-level declarations.+This is used for declaration that don't live in a module+(e.g., define on the command line.)++We assume that these declarations do not contain any nested modules.+-} renameTopDecls ::   ModName -> [TopDecl PName] -> RenameM (NamingEnv,[TopDecl Name]) renameTopDecls m ds0 =-  do let ds = snd (addImplicitNestedImports ds0)-     let mpath = TopModule m-     env    <- liftSupply (defsOf (map (InModule (Just mpath)) ds))-     nested <- liftSupply (collectNestedModulesDecls env m ds) -     setNestedModule (nestedModuleNames nested)-       do ds1 <- shadowNames' CheckOverlap env-                                        (renameTopDecls' (nested,mpath) ds)-          -- record a use of top-level names to avoid-          -- unused name warnings-          let exports = concatMap exportedNames ds1-          mapM_ recordUse (foldMap (exported NSType) exports)+  do -- Step 1: add implicit imports+     let ds = addImplicitNestedImports ds0 -          pure (env,ds1)+     -- Step 2: compute what's defined+     (defs,errs) <- liftSupply (modBuilder (topDeclsDefs (TopModule m) ds))+     mapM_ recordError errs --- | Returns declarations with additional imports and the public module names--- of this module and its children-addImplicitNestedImports ::-  [TopDecl PName] -> ([[Ident]], [TopDecl PName])-addImplicitNestedImports decls = (concat exportedMods, concat newDecls ++ other)-  where-  (mods,other)            = foldr classify ([], []) decls-  (newDecls,exportedMods) = unzip (map processModule mods)-  processModule m =-    let NestedModule m1 = tlValue m-        (childExs, ds1) = addImplicitNestedImports (mDecls m1)-        mname           = getIdent (thing (mName m1))-        imps            = map (mname :) ([] : childExs)-        isToName is     = case is of-                            [i] -> mkUnqual i-                            _   -> mkQual (isToQual (init is)) (last is)-        isToQual is     = packModName (map identText is)-        mkImp xs        = DImport-                          Located-                            { srcRange = srcRange (mName m1)-                            , thing = Import-                                        { iModule = ImpNested (isToName xs)-                                        , iAs     = Just (isToQual xs)-                                        , iSpec   = Nothing-                                        }-                            }-    in ( DModule m { tlValue = NestedModule m1 { mDecls = ds1 } }-       : map mkImp imps-       , case tlExport m of-           Public  -> imps-           Private -> []-       )+     -- Step 3: resolve imports+     extern       <- getExternal+     resolvedMods <- liftSupply (resolveImports extern (TopMod m defs)) +     let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)+                                   | ImpNested x <- Map.keys resolvedMods ] -  classify d (ms,ds) =-    case d of-      DModule tl -> (tl : ms, ds)-      _          -> (ms, d : ds) +     setResolvedLocals resolvedMods $+      setNestedModule pathToName+      do env    <- rmodDefines <$> lookupResolved (ImpTop m) -nestedModuleNames :: NestedMods -> Map ModPath Name-nestedModuleNames mp = Map.fromList (map entry (Map.keys mp))-  where-  entry n = case nameInfo n of-              Declared p _ -> (Nested p (nameIdent n),n)-              _ -> panic "nestedModuleName" [ "Not a top-level name" ]+         -- we already checked for duplicates in Step 2+         ds1 <- shadowNames' CheckNone env (renameTopDecls' ds)+         -- record a use of top-level names to avoid+         -- unused name warnings+         let exports = exportedDecls ds1+         mapM_ recordUse (exported NSType exports) +         pure (env,ds1) +--------------------------------------------------------------------------------+-- Stuff below is related to Step 4 of the algorithm.++ class Rename f where   rename :: f PName -> RenameM (f Name)  --- | Returns:+-- | This is used for both top-level and nested modules.+-- Returns: -----    * Interfaces for imported things,---    * Things defines in the module+--    * Things defined in the module --    * Renamed module renameModule' ::-  NestedMods -> NamingEnv -> ModPath -> ModuleG mname PName ->+  ImpName Name {- ^ Resolved name for this module -} ->+  ModuleG mname PName ->   RenameM (NamingEnv, ModuleG mname Name)-renameModule' thisNested env mpath m =-  setCurMod mpath-  do (moreNested,imps) <- mconcat <$> mapM doImport (mImports m)-     let allNested = Map.union moreNested thisNested-         openDs    = map thing (mSubmoduleImports m)-         allImps   = openLoop allNested env openDs imps+renameModule' mname m =+  setCurMod+    case mname of+      ImpTop r    -> TopModule r+      ImpNested r -> Nested (nameModPath r) (nameIdent r) -     (inScope,decls') <--        shadowNames' CheckNone allImps $-        shadowNames' CheckOverlap env $-                          -- maybe we should allow for a warning-                          -- if a local name shadows an imported one?-        do inScope <- getNamingEnv-           ds      <- renameTopDecls' (allNested,mpath) (mDecls m)-           pure (inScope, ds)-     let m1      = m { mDecls = decls' }-         exports = modExports m1-     mapM_ recordUse (exported NSType exports)-     return (inScope, m1)+  do resolved <- lookupResolved mname+     shadowNames' CheckNone (rmodImports resolved) +       case mDef m of +         NormalModule ds ->+            do let env = rmodDefines resolved+               (paramEnv,params) <-+                   shadowNames' CheckNone env+                      (doModParams (mModParams m))++               -- we check that defined names and ones that came+               -- from parameters do not clash, as this would be+               -- very confusing.+               shadowNames' CheckOverlap (env <> paramEnv) $+                  setModParams params+                  do ds1 <- renameTopDecls' ds+                     let exports = exportedDecls ds1+                     mapM_ recordUse (exported NSType exports)+                     inScope <- getNamingEnv+                     pure (inScope, m { mDef = NormalModule ds1 })++         -- The things defined by this module are the *results*+         -- of the instantiation, so we should *not* add them+         -- in scope when resolving.+         FunctorInstance f as _ ->+           do f'  <- rnLocated rename f+              as' <- rename as+              checkFunctorArgs as'++              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++              pure (inScope, m { mDef = FunctorInstance f' as' imap })++         InterfaceModule s ->+           shadowNames' CheckNone (rmodDefines resolved)+             do d <- InterfaceModule <$> renameIfaceModule mname s+                inScope <- getNamingEnv+                pure (inScope, m { mDef = d })+++checkFunctorArgs :: ModuleInstanceArgs Name -> RenameM ()+checkFunctorArgs args =+  case args of+    DefaultInstAnonArg {} ->+      panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"]+    DefaultInstArg l -> checkArg l+    NamedInstArgs as -> mapM_ checkNamedArg as+  where+  checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l++  checkArg l =+      case thing l of+        ModuleArg m+          | isFakeName m -> pure ()+          | otherwise    -> checkIsModule (srcRange l) m AModule+        ParameterArg {} -> pure () -- we check these in the type checker+        AddParams -> pure ()++mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name ->+  RenameM (Map Name Name)+mkInstMap checkFun acc0 ogname iname+  | isFakeName ogname = pure Map.empty+  | otherwise =+  do case checkFun of+       Nothing -> pure ()+       Just r  -> checkIsModule r ogname AFunctor+     (onames,osubs) <- lookupDefinesAndSubs ogname+     inames         <- lookupDefines iname+     let mp   = zipByTextName onames inames+         subs = [ (ImpNested k, ImpNested v)+                | k <- Set.toList osubs, Just v <- [Map.lookup k mp]+                ]+     foldM doSub (Map.union mp acc0) subs++  where+  doSub acc (k,v) = mkInstMap Nothing acc k v++++-- | This is used to rename local declarations (e.g. `where`) renameDecls :: [Decl PName] -> RenameM [Decl Name] renameDecls ds =   do (ds1,deps) <- depGroup (traverse rename ds)@@ -192,14 +340,37 @@              CyclicSCC ds_xs ->                let (rds,xs) = unzip ds_xs                in case mapM validRecursiveD rds of-                    Nothing -> do record (InvalidDependency xs)+                    Nothing -> do recordError (InvalidDependency xs)                                   pure rds                     Just bs ->                       do checkSameModule xs                          pure [DRec bs]      concat <$> mapM fromSCC ordered +-- | Rename declarations in a signature (i.e., type/prop synonyms)+renameSigDecls :: [SigDecl PName] -> RenameM [SigDecl Name]+renameSigDecls ds =+  do (ds1,deps) <- depGroup (traverse rename ds)+     let toNode d = let nm = case d of+                               SigTySyn ts _   -> thing (tsName ts)+                               SigPropSyn ps _ -> thing (psName ps)+                        x = NamedThing nm+                    in ((d,x), x, map NamedThing+                            $ Set.toList+                            $ Map.findWithDefault Set.empty x deps)+         ordered = toList (stronglyConnComp (map toNode ds1))+         fromSCC x =+           case x of+             AcyclicSCC (d,_) -> pure [d]+             CyclicSCC ds_xs ->+               do let (rds,xs) = unzip ds_xs+                  recordError (InvalidDependency xs)+                  pure rds +     concat <$> mapM fromSCC ordered+++ validRecursiveD :: Decl name -> Maybe (Bind name) validRecursiveD d =   case d of@@ -212,24 +383,128 @@   case ms of     a : as | let bad = [ fst b | b <- as, snd a /= snd b ]            , not (null bad) ->-              record $ InvalidDependency $ map NamedThing $ fst a : bad+              recordError (InvalidDependency $ map NamedThing $ fst a : bad)     _ -> pure ()   where-  ms = [ (x,p) | NamedThing x <- xs, Declared p _ <- [ nameInfo x ] ]+  ms = [ (x,ogModule og)+       | NamedThing x <- xs, GlobalName _ og <- [ nameInfo x ]+       ]  -renameTopDecls' ::-  (NestedMods,ModPath) -> [TopDecl PName] -> RenameM [TopDecl Name]-renameTopDecls' info ds =-  do (ds1,deps) <- depGroup (traverse (renameWithMods info) ds) +{- NOTE: Dependencies on Top Level Constraints+   =========================================== -     let (noNameDs,nameDs) = partitionEithers (map topDeclName ds1)-         ctrs = [ nm | (_,nm@(ConstratintAt {})) <- nameDs ]-         toNode (d,x) = ((d,x),x, (if usesCtrs d then ctrs else []) ++-                               map NamedThing-                             ( Set.toList-                             ( Map.findWithDefault Set.empty x deps) ))+For the new module system, things using a parameter depend on the parameter+declaration (i.e., `import signature`), which depends on the signature,+so dependencies on constraints in there should be OK.++However, we'd like to have a mechanism for declaring top level constraints in+a functor, that can impose constraints across types from *different*+parameters.  For the moment, we reuse `parameter type constraint C` for this.++Such constraints need to be:+  1. After the signature import+  2. After any type synonyms/newtypes using the parameters+  3. Before any value or type declarations that need to use the parameters.++Note that type declarations used by a constraint cannot use the constraint,+so they need to be well formed without it.++For other types, we use the following rule to determine if they use a+constraint:++  If:+    1. We have a constraint and type declaration+    2. They both mention the same type parameter+    3. There is no explicit dependency of the constraint on the DECL+  Then:+    The type declaration depends on the constraint.++Example:++  type T = 10             // Does not depend on anything so can go first++  signature A where+    type n : #++  import signature A     // Depends on A, so need to be after A++  parameter type constraint n > T+                        // Depends on the import (for @n@) and T++  type Q = [n-T]        // Depends on the top-level constraint+-}++++-- This assumes imports have already been processed+renameTopDecls' :: [TopDecl PName] -> RenameM [TopDecl Name]+renameTopDecls' ds =+  do -- rename and compute what names we depend on+     (ds1,deps) <- depGroup (traverse rename ds)++     fromParams <- getNamesFromModParams+     localParams <- getLocalModParamDeps++     let rawDepsFor x = Map.findWithDefault Set.empty x deps++         isTyParam x = nameNamespace x == NSType && x `Map.member` fromParams+++         (noNameDs,nameDs) = partitionEithers (map topDeclName ds1)+         ctrs = [ nm | (_,nm@(ConstratintAt {}),_) <- nameDs ]+         indirect = Map.fromList [ (y,x)+                                 | (_,x,ys) <- nameDs, y <- ys ]+         mkDepName x = case Map.lookup x fromParams of+                         Just dn -> dn+                         Nothing -> NamedThing x+         depsFor x =+           [ Map.findWithDefault (mkDepName y) (NamedThing y) indirect+           | y <- Set.toList (Map.findWithDefault Set.empty x deps)+           ]++         {- See [NOTE: Dependencies on Top Level Constraints] -}+         addCtr nm ctr =+            case nm of+              NamedThing x+                | nameNamespace x == NSType+                , let ctrDeps = rawDepsFor ctr+                      tyDeps  = rawDepsFor nm+                , not (x `Set.member` ctrDeps)+                , not (Set.null (Set.intersection+                                      (Set.filter isTyParam ctrDeps)+                                      (Set.filter isTyParam tyDeps)))+                  -> Just ctr+              _ -> Nothing++         addCtrs (d,x)+          | usesCtrs d = ctrs+          | otherwise  = mapMaybe (addCtr x) ctrs++         addModParams d =+           case d of+             DModule tl | NestedModule m <- tlValue tl+                        , FunctorInstance _ as _ <- mDef m ->+               case as of+                  DefaultInstArg arg -> depsOfArg arg+                  NamedInstArgs args -> concatMap depsOfNamedArg args+                  DefaultInstAnonArg {} -> []++               where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a+                     depsOfArg a = case thing a of+                                     AddParams -> []+                                     ModuleArg {} -> []+                                     ParameterArg p ->+                                       case Map.lookup p localParams of+                                         Just i -> [i]+                                         Nothing -> []+             _ -> []++         toNode (d,x,_) = ((d,x),x, addCtrs (d,x) +++                                    addModParams d +++                                    depsFor x)+          ordered = stronglyConnComp (map toNode nameDs)          fromSCC x =             case x of@@ -237,7 +512,7 @@               CyclicSCC ds_xs ->                 let (rds,xs) = unzip ds_xs                 in case mapM valid rds of-                     Nothing -> do record (InvalidDependency xs)+                     Nothing -> do recordError (InvalidDependency xs)                                    pure rds                      Just bs ->                        do checkSameModule xs@@ -253,36 +528,49 @@      rds <- mapM fromSCC ordered      pure (concat (noNameDs:rds))   where++  -- This indicates if a declaration might depend on the constraints in scope.+  -- Since uses of constraints are not implicitly named, value declarations+  -- are assumed to potentially use the constraints.++  -- XXX: This is inaccurate, and *I think* it amounts to checking that something+  -- is in the value namespace.   Perhaps the rule should be that a value+  -- depends on a parameter constraint if it mentions at least one+  -- type parameter somewhere.++  -- XXX: Besides, types might need constraints for well-formedness...+  -- This is just bogus+  -- Although not that type/prop synonyms may be defined wherever as they+  -- keep the validity constraints they need and emit them at the *use* sites.   usesCtrs td =     case td of       Decl tl                 -> isValDecl (tlValue tl)       DPrimType {}            -> False       TDNewtype {}            -> False-      DParameterType {}       -> False-      DParameterConstraint {} -> False--      DParameterFun {}        -> True-      -- Here we may need the constraints to validate the type-      -- (e.g., if the parameter is of type `Z a`)+      DParamDecl {}           -> False+      DInterfaceConstraint {} -> False         DModule tl              -> any usesCtrs (mDecls m)         where NestedModule m = tlValue tl       DImport {}              -> False+      DModParam {}            -> False    -- no definitions here       Include {}              -> bad "Include"    isValDecl d =     case d of       DLocated d' _ -> isValDecl d'       DBind {}      -> True+      DRec {}       -> True+       DType {}      -> False       DProp {}      -> False-      DRec {}       -> True-      DSignature {} -> bad "DSignature"-      DFixity {}    -> bad "DFixity"-      DPragma {}    -> bad "DPragma"-      DPatBind {}   -> bad "DPatBind" +      DSignature {}       -> bad "DSignature"+      DFixity {}          -> bad "DFixity"+      DPragma {}          -> bad "DPragma"+      DPatBind {}         -> bad "DPatBind"+   bad msg = panic "renameTopDecls'" [msg]  @@ -302,172 +590,243 @@   where   bad x = panic "declName" [x] -topDeclName :: TopDecl Name -> Either (TopDecl Name) (TopDecl Name, DepName)+topDeclName ::+  TopDecl Name ->+  Either (TopDecl Name) (TopDecl Name, DepName, [DepName]) topDeclName topDecl =   case topDecl of     Decl d                  -> hasName (declName (tlValue d))     DPrimType d             -> hasName (thing (primTName (tlValue d)))-    TDNewtype d             -> hasName (thing (nName (tlValue d)))-    DParameterType d        -> hasName (thing (ptName d))-    DParameterFun d         -> hasName (thing (pfName d))+    TDNewtype d             -> hasName' (thing (nName (tlValue d)))+                                        [ nConName (tlValue d) ]     DModule d               -> hasName (thing (mName m))       where NestedModule m = tlValue d -    DParameterConstraint ds ->-      case ds of-        []  -> noName-        _   -> Right (topDecl, ConstratintAt (fromJust (getLoc ds)))+    DInterfaceConstraint _ ds -> special (ConstratintAt (srcRange ds))+     DImport {}              -> noName +    DModParam m             -> special (ModParamName (srcRange (mpSignature m))+                                                     (mpName m))+     Include {}              -> bad "Include"+    DParamDecl {}           -> bad "DParamDecl"   where   noName    = Left topDecl-  hasName n = Right (topDecl, NamedThing n)+  hasName n = hasName' n []+  hasName' n ms = Right (topDecl, NamedThing n, map NamedThing ms)+  special x = Right (topDecl, x, [])   bad x     = panic "topDeclName" [x]  --- | Returns:---  * The public interface of the imported module---  * Infromation about nested modules in this module---  * New names introduced through this import-doImport :: Located Import -> RenameM (NestedMods, NamingEnv)-doImport li =-  do let i = thing li-     decls <- lookupImport i-     let declsOf = unqualifiedEnv . ifPublic-         nested  = declsOf <$> ifModules decls-     pure (nested, interpImportIface i decls)  +{- | Compute the names introduced by a module parameter.+This should be run in a context containing everything that's in scope+except for the module parameters.  We don't need to compute a fixed point here+because the signatures (and hence module parameters) cannot contain signatures. ------------------------------------------------------------------------------------ Compute names coming through `open` statements.+The resulting naming environment contains the new names introduced by this+parameter.+-}+doModParam ::+  ModParam PName ->+  RenameM (NamingEnv, RenModParam)+doModParam mp =+  do let sigName = mpSignature mp+         loc     = srcRange sigName+     withLoc loc+       do me <- getCurMod -data OpenLoopState = OpenLoopState-  { unresolvedOpen  :: [ImportG PName]-  , scopeImports    :: NamingEnv    -- names from open/impot-  , scopeDefs       :: NamingEnv    -- names defined in this module-  , scopingRel      :: NamingEnv    -- defs + imports with shadowing-                                    -- (just a cache)-  , openLoopChange  :: Bool-  }+          (sigName',isFake) <-+             case thing sigName of+               ImpTop t -> pure (ImpTop t, False)+                -- XXX: should we record a dependency here?+                -- Not sure what the dependencies are for.. --- | Processing of a single @open@ declaration-processOpen :: NestedMods -> OpenLoopState -> ImportG PName -> OpenLoopState-processOpen modEnvs s o =-  case lookupNS NSModule (iModule o) (scopingRel s) of-    []  -> s { unresolvedOpen = o : unresolvedOpen s }-    [n] ->-      case Map.lookup n modEnvs of-        Nothing  -> panic "openLoop" [ "Missing defintion for module", show n ]-        Just def ->-          let new = interpImportEnv o def-              newImps = new <> scopeImports s-          in s { scopeImports   = newImps-               , scopingRel     = scopeDefs s `shadowing` newImps-               , openLoopChange = True-               }-    _ -> s-    {- Notes:-       * ambiguity will be reported later when we do the renaming-       * assumes scoping only grows, which should be true-       * we are not adding the names from *either* of the imports-         so this may give rise to undefined names, so we may want to-         suppress reporing undefined names if there ambiguities for-         module names.  Alternatively we could add the defitions from-         *all* options, but that might lead to spurious ambiguity errors.-    -}+               ImpNested n ->+                 do mb <- resolveNameMaybe NameUse NSModule n+                    (nm,isFake) <- case mb of+                                     Just rnm -> pure (rnm,False)+                                     Nothing ->+                                       do rnm <- reportUnboundName NSModule n+                                          pure (rnm,True)+                    case modPathCommon me (nameModPath nm) of+                      Just (_,[],_) ->+                        recordError+                           (InvalidDependency [ModPath me, NamedThing nm])+                      _ -> pure ()+                    pure (ImpNested nm, isFake) -{- | Complete the set of import using @open@ declarations.-This should terminate because on each iteration either @unresolvedOpen@-decreases or @openLoopChange@ remians @False@. We don't report errors-here, as they will be reported during renaming anyway. -}-openLoop ::-  NestedMods      {- ^ Definitions of all known nested modules  -} ->-  NamingEnv       {- ^ Definitions of the module (these shadow) -} ->-  [ImportG PName] {- ^ Open declarations                        -} ->-  NamingEnv       {- ^ Imported declarations                    -} ->-  NamingEnv       {- ^ Completed imports                        -}-openLoop modEnvs defs os imps =-  scopingRel $ loop OpenLoopState-                      { unresolvedOpen = os-                      , scopeImports   = imps-                      , scopeDefs      = defs-                      , scopingRel     = defs `shadowing` imps-                      , openLoopChange = True-                      }-  where-  loop s-    | openLoopChange s =-      loop $ foldl' (processOpen modEnvs)-                    s { unresolvedOpen = [], openLoopChange = False }-                    (unresolvedOpen s)-    | otherwise = s+          unless isFake+            (checkIsModule (srcRange sigName) sigName' ASignature)+          sigEnv <- if isFake then pure mempty else lookupDefines sigName'  +          {- XXX: It seems a bit odd to use "newModParam" for the names to+             be used for the instantiated type synonyms,+             but what other name could we use? -}+          let newP x = do y <- lift (newModParam me (mpName mp) loc x)+                          sets_ (Map.insert y x)+                          pure y+          (newEnv',nameMap) <- runStateT Map.empty (travNamingEnv newP sigEnv)+          let paramName = mpAs mp+          let newEnv = case paramName of+                         Nothing -> newEnv'+                         Just q  -> qualify q newEnv'+          pure ( newEnv+               , RenModParam+                 { renModParamName     = mpName mp+                 , renModParamRange    = loc+                 , renModParamSig      = sigName'+                 , renModParamInstance = nameMap+                 }+               )++{- | Process the parameters of a module.+Should be executed in a context where everything's already in the context,+except the module parameters.+-}+doModParams :: [ModParam PName] -> RenameM (NamingEnv, [RenModParam])+doModParams srcParams =+  do (paramEnvs,params) <- unzip <$> mapM doModParam  srcParams++     let repeated = groupBy ((==) `on` renModParamName)+                  $ sortBy (compare `on` renModParamName) params++     forM_ repeated \ps ->+       case ps of+         [_]      -> pure ()+         ~(p : _) -> recordError (MultipleModParams (renModParamName p)+                                                    (map renModParamRange ps))++     pure (mconcat paramEnvs,params)++++ -------------------------------------------------------------------------------- +rnLocated :: (a -> RenameM b) -> Located a -> RenameM (Located b)+rnLocated f loc = withLoc loc $+  do a' <- f (thing loc)+     return loc { thing = a' } -data WithMods f n = WithMods (NestedMods,ModPath) (f n) -forgetMods :: WithMods f n -> f n-forgetMods (WithMods _ td) = td -renameWithMods ::-  Rename (WithMods f) => (NestedMods,ModPath) -> f PName -> RenameM (f Name)-renameWithMods info m = forgetMods <$> rename (WithMods info m)  -instance Rename (WithMods TopDecl) where-  rename (WithMods info td) = WithMods info <$>++instance Rename TopDecl where+  rename td =     case td of-      Decl d      -> Decl      <$> traverse rename d-      DPrimType d -> DPrimType <$> traverse rename d-      TDNewtype n -> TDNewtype <$> traverse rename n-      Include n   -> return (Include n)-      DParameterFun f  -> DParameterFun  <$> rename f-      DParameterType f -> DParameterType <$> rename f+      Decl d            -> Decl      <$> traverse rename d+      DPrimType d       -> DPrimType <$> traverse rename d+      TDNewtype n       -> TDNewtype <$> traverse rename n+      Include n         -> return (Include n)+      DModule m  -> DModule <$> traverse rename m+      DImport li -> DImport <$> renI li+      DModParam mp -> DModParam <$> rename mp+      DInterfaceConstraint d ds ->+        depsOf (ConstratintAt (srcRange ds))+        (DInterfaceConstraint d <$> rnLocated (mapM rename) ds)+      DParamDecl {} -> panic "rename" ["DParamDecl"] -      DParameterConstraint ds ->-        case ds of-          [] -> pure (DParameterConstraint [])-          _  -> depsOf (ConstratintAt (fromJust (getLoc ds)))-              $ DParameterConstraint <$> mapM renameLocated ds-      DModule m -> DModule <$> traverse (renameWithMods info) m-      DImport li -> DImport <$> traverse renI li-        where-        renI i = do m <- rename (iModule i)-                    pure i { iModule = m } ++renI :: Located (ImportG (ImpName PName)) ->+        RenameM (Located (ImportG (ImpName Name)))+renI li =+  withLoc (srcRange li)+  do m <- rename (iModule i)+     unless (isFakeName m) (recordImport (srcRange li) m)+     pure li { thing = i { iModule = m } }+  where+  i = thing li+++instance Rename ModParam where+  rename mp =+    do x   <- rnLocated rename (mpSignature mp)+       depsOf (ModParamName (srcRange (mpSignature mp)) (mpName mp))+         do ren <- renModParamInstance <$> getModParam (mpName mp)++            {- Here we add 2 "uses" to all type-level names introduced,+               so that we don't get unused warnings for type parameters.+             -}+            mapM_ recordUse [ s | t <- Map.keys ren, nameNamespace t == NSType+                                , s <- [t,t] ]++            pure mp { mpSignature = x, mpRenaming = ren }+++renameIfaceModule :: ImpName Name -> Signature PName -> RenameM (Signature Name)+renameIfaceModule nm sig =+  do env <- rmodDefines <$> lookupResolved nm+     let depName = case nm of+                     ImpNested n -> NamedThing n+                     ImpTop t    -> ModPath (TopModule t)+     shadowNames' CheckOverlap env $+        depsOf depName+        do imps <- traverse renI (sigImports sig)+           tps <- traverse rename (sigTypeParams sig)++           ds  <- renameSigDecls (sigDecls sig)+           cts <- traverse (rnLocated rename) (sigConstraints sig)+           fun <- traverse rename (sigFunParams sig)++           -- we record a use here to avoid getting a warning in interfaces+           -- that declare only types, and so appear "unused".+           forM_ tps \tp -> recordUse (thing (ptName tp))+           forM_ ds  \d  -> recordUse $ case d of+                                          SigTySyn ts _ -> thing (tsName ts)+                                          SigPropSyn ps _ -> thing (psName ps)++           pure Signature+                  { sigImports      = imps+                  , sigTypeParams   = tps+                  , sigDecls        = ds+                  , sigConstraints  = cts+                  , sigFunParams    = fun+                  }+ instance Rename ImpName where   rename i =     case i of       ImpTop m -> pure (ImpTop m)       ImpNested m -> ImpNested <$> resolveName NameUse NSModule m -instance Rename (WithMods NestedModule) where-  rename (WithMods info (NestedModule m)) = WithMods info <$>-    do let (nested,mpath) = info-           lnm            = mName m+instance Rename ModuleInstanceArgs where+  rename args =+    case args of+      DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a+      NamedInstArgs xs -> NamedInstArgs  <$> traverse rename xs+      DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"]++instance Rename ModuleInstanceNamedArg where+  rename (ModuleInstanceNamedArg x m) =+    ModuleInstanceNamedArg x <$> rnLocated rename m++instance Rename ModuleInstanceArg where+  rename arg =+    case arg of+      ModuleArg m -> ModuleArg <$> rename m+      ParameterArg a -> pure (ParameterArg a)+      AddParams -> pure AddParams++instance Rename NestedModule where+  rename (NestedModule m) =+    do let lnm            = mName m            nm             = thing lnm-           newMPath       = Nested mpath (getIdent nm)        n   <- resolveName NameBind NSModule nm        depsOf (NamedThing n)-         do let env = case Map.lookup n (fst info) of-                        Just defs -> defs-                        Nothing -> panic "rename"-                           [ "Missing environment for nested module", show n ]-            -- XXX: we should store in scope somehwere if we want to browse+         do -- XXX: we should store in scope somewhere if we want to browse             -- nested modules properly-            (_inScope,m1) <- renameModule' nested env newMPath m+            let m' = m { mName = ImpNested <$> mName m }+            (_inScope,m1) <- renameModule' (ImpNested n) m'             pure (NestedModule m1 { mName = lnm { thing = n } })  -renameLocated :: Rename f => Located (f PName) -> RenameM (Located (f Name))-renameLocated x =-  do y <- rename (thing x)-     return x { thing = y }- instance Rename PrimType where   rename pt =     do x <- rnLocated (renameType NameBind) (primTName pt)@@ -477,7 +836,7 @@              -- Record an additional use for each parameter since we checked             -- earlier that all the parameters are used exactly once in the-            -- body of the signature.  This prevents incorret warnings+            -- body of the signature.  This prevents incorrect warnings             -- about unused names.             mapM_ (recordUse . tpName) (fst cts) @@ -495,10 +854,11 @@          do sig' <- renameSchema (pfSchema a)             return a { pfName = n', pfSchema = snd sig' } -rnLocated :: (a -> RenameM b) -> Located a -> RenameM (Located b)-rnLocated f loc = withLoc loc $-  do a' <- f (thing loc)-     return loc { thing = a' }+instance Rename SigDecl where+  rename decl =+    case decl of+      SigTySyn ts mb   -> SigTySyn      <$> rename ts <*> pure mb+      SigPropSyn ps mb -> SigPropSyn    <$> rename ps <*> pure mb  instance Rename Decl where   rename d      = case d of@@ -509,7 +869,7 @@     DLocated d' r     -> withLoc r                        $ DLocated      <$> rename d'  <*> pure r -    DFixity{}         -> panic "renaem" [ "DFixity" ]+    DFixity{}         -> panic "rename" [ "DFixity" ]     DSignature {}     -> panic "rename" [ "DSignature" ]     DPragma  {}       -> panic "rename" [ "DPragma" ]     DPatBind {}       -> panic "rename" [ "DPatBind " ]@@ -520,11 +880,16 @@ instance Rename Newtype where   rename n      =     shadowNames (nParams n) $-    do name' <- rnLocated (renameType NameBind) (nName n)-       depsOf (NamedThing (thing name')) $+    do nameT <- rnLocated (renameType NameBind) (nName n)+       nameC <- renameVar  NameBind (nConName n)++       depsOf (NamedThing nameC) (addDep (thing nameT))++       depsOf (NamedThing (thing nameT)) $          do ps'   <- traverse rename (nParams n)             body' <- traverse (traverse rename) (nBody n)-            return Newtype { nName   = name'+            return Newtype { nName   = nameT+                           , nConName = nameC                            , nParams = ps'                            , nBody   = body' } @@ -539,42 +904,57 @@                  NSType -> recordUse                  _      -> const (pure ())      case lkpIn expected of-       Just [n]  ->-          do case nt of-               NameBind -> pure ()-               NameUse  -> addDep n-             use n    -- for warning-             return (Just n)-       Just []   -> panic "Renamer" ["Invalid expression renaming environment"]-       Just syms ->-         do mapM_ use syms    -- mark as used to avoid unused warnings-            n <- located qn-            record (MultipleSyms n syms)-            return (Just (head syms))+       Just xs ->+         case xs of+          One n ->+            do case nt of+                 NameBind -> pure ()+                 NameUse  -> addDep n+               use n    -- for warning+               return (Just n)+          Ambig symSet ->+            do let syms = Set.toList symSet+               mapM_ use syms    -- mark as used to avoid unused warnings+               n <- located qn+               recordError (MultipleSyms n syms)+               return (Just (head syms))         Nothing -> pure Nothing +reportUnboundName :: Namespace -> PName -> RenameM Name+reportUnboundName expected qn =+  do ro <- RenameM ask+     let lkpIn here = Map.lookup qn (namespaceMap here (roNames ro))+         others     = [ ns | ns <- allNamespaces+                           , ns /= expected+                           , Just _ <- [lkpIn ns] ]+     nm <- located qn+     case others of+       -- name exists in a different namespace+       actual : _ -> recordError (WrongNamespace expected actual nm)++       -- the value is just missing+       [] -> recordError (UnboundName expected nm)++     mkFakeName expected qn++isFakeName :: ImpName Name -> Bool+isFakeName m =+  case m of+    ImpTop x -> x == undefinedModName+    ImpNested x ->+      case nameTopModuleMaybe x of+        Just y  -> y == undefinedModName+        Nothing -> False++ -- | Resolve a name, and report error on failure resolveName :: NameType -> Namespace -> PName -> RenameM Name resolveName nt expected qn =   do mb <- resolveNameMaybe nt expected qn      case mb of        Just n -> pure n-       Nothing ->-         do ro <- RenameM ask-            let lkpIn here = Map.lookup qn (namespaceMap here (roNames ro))-                others     = [ ns | ns <- allNamespaces-                                  , ns /= expected-                                  , Just _ <- [lkpIn ns] ]-            nm <- located qn-            case others of-              -- name exists in a different namespace-              actual : _ -> record (WrongNamespace expected actual nm)--              -- the value is just missing-              [] -> record (UnboundName expected nm)--            mkFakeName expected qn+       Nothing -> reportUnboundName expected qn   renameVar :: NameType -> PName -> RenameM Name@@ -590,7 +970,8 @@ mkFakeName :: Namespace -> PName -> RenameM Name mkFakeName ns pn =   do ro <- RenameM ask-     liftSupply (mkParameter ns (getIdent pn) (roLoc ro))+     liftSupply (mkDeclared ns (TopModule undefinedModName)+                               SystemName (getIdent pn) Nothing (roLoc ro))  -- | Rename a schema, assuming that none of its type variables are already in -- scope.@@ -639,7 +1020,7 @@       TTuple fs      -> TTuple   <$> traverse rename fs       TWild          -> return TWild       TLocated t' r  -> withLoc r (TLocated <$> rename t' <*> pure r)-      TParens t'     -> TParens <$> rename t'+      TParens t' k   -> (`TParens` k) <$> rename t'       TInfix a o _ b -> do o' <- renameTypeOp o                            a' <- rename a                            b' <- rename b@@ -653,7 +1034,7 @@     FCLeft  -> return (TInfix t o2 f2 z)     FCRight -> do r <- mkTInfix y op z                   return (TInfix x o1 f1 r)-    FCError -> do record (FixityError o1 f1 o2 f2)+    FCError -> do recordError (FixityError o1 f1 o2 f2)                   return (TInfix t o2 f2 z)  mkTInfix (TLocated t' _) op z =@@ -683,8 +1064,14 @@  instance Rename BindDef where   rename DPrim     = return DPrim+  rename DForeign  = return DForeign   rename (DExpr e) = DExpr <$> rename e+  rename (DPropGuards cases) = DPropGuards <$> traverse rename cases +instance Rename PropGuardCase where+  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@@ -712,7 +1099,8 @@        case more of          [] -> case h of                  UpdSet -> UpdField UpdSet [l] <$> rename e-                 UpdFun -> UpdField UpdFun [l] <$> rename (EFun emptyFunDesc [PVar p] e)+                 UpdFun -> UpdField UpdFun [l] <$>+                                        rename (EFun emptyFunDesc [PVar p] e)                        where                        p = UnQual . selName <$> last ls          _ -> UpdField UpdFun [l] <$> rename (EUpd Nothing [ UpdField h more e])@@ -728,9 +1116,6 @@   rename expr = case expr of     EVar n          -> EVar <$> renameVar NameUse n     ELit l          -> return (ELit l)-    ENeg e          -> ENeg    <$> rename e-    EComplement e   -> EComplement-                               <$> rename e     EGenerate e     -> EGenerate                                <$> rename e     ETuple es       -> ETuple  <$> traverse rename es@@ -786,6 +1171,7 @@                           x' <- rename x                           z' <- rename z                           mkEInfix x' op z'+    EPrefix op e    -> EPrefix op <$> rename e   checkLabels :: [UpdField PName] -> RenameM ()@@ -795,7 +1181,7 @@    check done l =     do case find (overlap l) done of-         Just l' -> record (OverlappingRecordUpdate (reLoc l) (reLoc l'))+         Just l' -> recordError (OverlappingRecordUpdate (reLoc l) (reLoc l'))          Nothing -> pure ()        pure (l : done) @@ -827,9 +1213,25 @@      FCRight -> do r <- mkEInfix y op z                    return (EInfix x o1 f1 r) -     FCError -> do record (FixityError o1 f1 o2 f2)+     FCError -> do recordError (FixityError o1 f1 o2 f2)                    return (EInfix e o2 f2 z) +mkEInfix e@(EPrefix o1 x) op@(o2, f2) y =+  case compareFixity (prefixFixity o1) f2 of+    FCRight -> do+      let warning = PrefixAssocChanged o1 x o2 f2 y+      RenameM $ sets_ (\rw -> rw {rwWarnings = warning : rwWarnings rw})+      r <- mkEInfix x op y+      return (EPrefix o1 r)++    -- Even if the fixities conflict, we make the prefix operator take+    -- precedence.+    _ -> return (EInfix e o2 f2 y)++-- Note that for prefix operator on RHS of infix operator we make the prefix+-- operator always have precedence, so we allow a * -b instead of requiring+-- a * (-b).+ mkEInfix (ELocated e' _) op z =      mkEInfix e' op z @@ -921,9 +1323,9 @@ patternEnv  = go   where   go (PVar Located { .. }) =-    do n <- liftSupply (mkParameter NSValue (getIdent thing) srcRange)+    do n <- liftSupply (mkLocal NSValue (getIdent thing) srcRange)        -- XXX: for deps, we should record a use-       return (singletonE thing n)+       return (singletonNS NSValue thing n)    go PWild            = return mempty   go (PTuple ps)      = bindVars ps@@ -961,23 +1363,23 @@            -- of the type of the pattern.            | null ps ->              do loc <- curLoc-                n   <- liftSupply (mkParameter NSType (getIdent pn) loc)-                return (singletonT pn n)+                n   <- liftSupply (mkLocal NSType (getIdent pn) loc)+                return (singletonNS NSType pn n)             -- This references a type synonym that's not in scope. Record an            -- error and continue with a made up name.            | otherwise ->              do loc <- curLoc-                record (UnboundName NSType (Located loc pn))-                n   <- liftSupply (mkParameter NSType (getIdent pn) loc)-                return (singletonT pn n)+                recordError (UnboundName NSType (Located loc pn))+                n   <- liftSupply (mkLocal NSType (getIdent pn) loc)+                return (singletonNS NSType pn n)    typeEnv (TRecord fs)      = bindTypes (map snd (recordElements fs))   typeEnv (TTyApp fs)       = bindTypes (map value fs)   typeEnv (TTuple ts)       = bindTypes ts   typeEnv TWild             = return mempty   typeEnv (TLocated ty loc) = withLoc loc (typeEnv ty)-  typeEnv (TParens ty)      = typeEnv ty+  typeEnv (TParens ty _)    = typeEnv ty   typeEnv (TInfix a _ _ b)  = bindTypes [a,b]    bindTypes [] = return mempty@@ -1005,3 +1407,20 @@     shadowNames ps     do n' <- rnLocated (renameType NameBind) n        PropSyn n' <$> pure f <*> traverse rename ps <*> traverse rename cs++--------------------------------------------------------------------------------++instance PP RenamedModule where+  ppPrec _ rn = updPPCfg (\cfg -> cfg { ppcfgShowNameUniques = True }) doc+    where+    doc =+      vcat [ "// --- Defines -----------------------------"+           , pp (rmDefines rn)+           , "// --- In scope ----------------------------"+           , pp (rmInScope rn)+           , "// -- Module -------------------------------"+           , pp (rmModule rn)+           , "// -----------------------------------------"+           ]++