cryptol 3.1.0 → 3.2.0

raw patch · 52 files changed

+1772/−627 lines, 52 filesdep +file-embeddep −heredocdep ~sbvdep ~what4PVP ok

version bump matches the API change (PVP)

Dependencies added: file-embed

Dependencies removed: heredoc

Dependency ranges changed: sbv, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +44/−0
• bench/Main.hs +2/−2
• cryptol.cabal +5/−5
• cryptol/Main.hs +7/−7
• cryptol/REPL/Haskeline.hs +28/−27
• cryptol/REPL/Logo.hs +6/−1
• lib/Cryptol.cry +10/−10
• src/Cryptol/Backend/Arch.hs +2/−2
• src/Cryptol/Backend/FFI/Error.hs +5/−3
• src/Cryptol/Eval/FFI/GenHeader.hs +3/−3
• src/Cryptol/Eval/Reference.lhs +93/−21
• src/Cryptol/IR/FreeVars.hs +13/−2
• src/Cryptol/ModuleSystem.hs +14/−3
• src/Cryptol/ModuleSystem/Base.hs +26/−7
• src/Cryptol/ModuleSystem/Binds.hs +1/−1
• src/Cryptol/ModuleSystem/Env.hs +92/−14
• src/Cryptol/ModuleSystem/Interface.hs +22/−10
• src/Cryptol/ModuleSystem/Monad.hs +8/−5
• src/Cryptol/ModuleSystem/Name.hs +0/−1
• src/Cryptol/ModuleSystem/Names.hs +9/−1
• src/Cryptol/ModuleSystem/Renamer.hs +12/−3
• src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs +28/−18
• src/Cryptol/Parser.y +22/−17
• src/Cryptol/Parser/AST.hs +28/−12
• src/Cryptol/Parser/ExpandPropGuards.hs +153/−7
• src/Cryptol/Parser/Layout.hs +12/−4
• src/Cryptol/Parser/LexerUtils.hs +1/−1
• src/Cryptol/Parser/NoPat.hs +3/−3
• src/Cryptol/Parser/ParserUtils.hs +142/−50
• src/Cryptol/Parser/Unlit.hs +28/−13
• src/Cryptol/Prelude.hs +10/−12
• src/Cryptol/PrimeEC.hs +3/−3
• src/Cryptol/REPL/Command.hs +546/−157
• src/Cryptol/REPL/Help.hs +15/−12
• src/Cryptol/REPL/Monad.hs +53/−33
• src/Cryptol/Symbolic/SBV.hs +31/−15
• src/Cryptol/Symbolic/What4.hs +22/−4
• src/Cryptol/TypeCheck/AST.hs +77/−10
• src/Cryptol/TypeCheck/Error.hs +9/−32
• src/Cryptol/TypeCheck/Infer.hs +75/−63
• src/Cryptol/TypeCheck/Interface.hs +3/−2
• src/Cryptol/TypeCheck/Kind.hs +1/−1
• src/Cryptol/TypeCheck/Module.hs +16/−6
• src/Cryptol/TypeCheck/ModuleInstance.hs +7/−1
• src/Cryptol/TypeCheck/Monad.hs +15/−10
• src/Cryptol/TypeCheck/Sanity.hs +6/−2
• src/Cryptol/TypeCheck/SimpType.hs +15/−3
• src/Cryptol/TypeCheck/Solver/Numeric.hs +26/−0
• src/Cryptol/TypeCheck/Solver/SMT.hs +1/−0
• src/Cryptol/TypeCheck/Type.hs +9/−1
• src/Cryptol/Utils/Ident.hs +12/−6
• src/Cryptol/Utils/PP.hs +1/−1

@@ -1,3 +1,47 @@+# 3.2.0 -- 2024-08-20++## Language changes++* Add implicit imports for non-anonymous modules defined by functor+  instantiation.   For details, see #1691.++## Bug fixes++* Fix #1685, which caused Cryptol to panic when given a local definition without+  a type signature that uses numeric constraint guards.++* Fix #1593 and #1693, two related bugs that would cause Cryptol to panic when+  checking ill-typed constraint guards for exhaustivity.++* Fix #1675, which could cause `PrimeEC` to produce incorrect results.++* Fix #1489, which allows for the type checker to reason about exponents.++## New features++* New REPL command :focus enables specifying a submodule scope for evaluating+  expressions.++  ```repl+  :focus submodule M+  :browse+  ```++* New REPL command :check-docstrings extracts code-blocks from docstring+  comments from a module. Code blocks can be delimited with three-or-more+  backticks using the language "repl". Code blocks are evaluated in a local+  REPL context and checked to pass.++  ````cryptol+  /**+   * ```repl+   * :exhaust f+   * ```+   */+  f : [8] -> Bool+  f x = x + 1 - 1 == x+  ````+ # 3.1.0 -- 2024-02-05  ## Language changes

@@ -138,7 +138,7 @@         menv <- M.initialModuleEnv         (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do           m <- M.loadModuleByPath path-          M.setFocusedModule (T.mName m)+          M.setFocusedModule (P.ImpTop (T.mName m))           let Right pexpr = P.parseExpr expr           (_, texpr, _) <- M.checkExpr pexpr           return texpr@@ -160,7 +160,7 @@         menv <- M.initialModuleEnv         (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do           m <- M.loadModuleByPath path-          M.setFocusedModule (T.mName m)+          M.setFocusedModule (P.ImpTop (T.mName m))           let Right pexpr = P.parseExpr expr           (_, texpr, _) <- M.checkExpr pexpr           return texpr

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             3.1.0+Version:             3.2.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD-3-Clause@@ -27,7 +27,7 @@   type:     git   location: https://github.com/GaloisInc/cryptol.git   -- add a tag on release branches-  tag:      3.1.0+  tag: 3.2.0   flag static@@ -58,11 +58,11 @@                        deepseq           >= 1.3,                        directory         >= 1.2.2.0,                        exceptions,+                       file-embed        >= 0.0.16,                        filepath          >= 1.3,                        gitrev            >= 1.0,                        ghc-prim,                        GraphSCC          >= 1.0.4,-                       heredoc           >= 0.2,                        language-c99,                        language-c99-simple,                        libBF             >= 0.6 && < 0.7,@@ -74,7 +74,7 @@                        prettyprinter     >= 1.7.0,                        pretty-show,                        process           >= 1.2,-                       sbv               >= 9.1 && < 10.3,+                       sbv               >= 9.1 && < 10.11,                        simple-smt        >= 0.9.7,                        stm               >= 2.4,                        strict,@@ -85,7 +85,7 @@                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.4 && < 1.6+                       what4             >= 1.4 && < 1.7    if impl(ghc >= 9.0)     build-depends:     ghc-bignum        >= 1.0 && < 1.4

@@ -13,7 +13,7 @@  import OptParser -import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..))+import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandResult(..)) import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,                    io,prependSearchPath,setSearchPath,parseSearchPath) import qualified Cryptol.REPL.Monad as REPL@@ -25,7 +25,7 @@ import Cryptol.Utils.PP import Cryptol.Version (displayVersion) -import Control.Monad (when)+import Control.Monad (when, void) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)@@ -234,9 +234,9 @@             Nothing -> return ()             Just cmdFile -> removeFile cmdFile -          case status of-            CommandError -> exitFailure-            CommandOk    -> exitSuccess+          if crSuccess status+            then exitSuccess+            else exitFailure  setupCmdScript :: Options -> IO (Options, Maybe FilePath) setupCmdScript opts =@@ -283,7 +283,7 @@    case optLoad opts of     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x-    [l] -> loadCmd l `REPL.catch` \x -> do+    [l] -> void (loadCmd l) `REPL.catch` \x -> do              io $ print $ pp x              -- If the requested file fails to load, load the prelude instead...              loadPrelude `REPL.catch` \y -> do@@ -292,7 +292,7 @@              -- we tried, instead of the Prelude              REPL.setEditPath l              REPL.setLoadedMod REPL.LoadedModule-               { REPL.lName = Nothing+               { REPL.lFocus = Nothing                , REPL.lPath = InFile l                }     _   -> io $ putStrLn "Only one file may be loaded at the command line."

@@ -9,6 +9,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE BangPatterns #-} {-# OPTIONS_GHC -fno-warn-orphans #-}  module REPL.Haskeline where@@ -52,10 +53,10 @@  deriving (Show, Eq)  -- | One REPL invocation, either from a file or from the terminal.-crySession :: ReplMode -> Bool -> REPL CommandExitCode+crySession :: ReplMode -> Bool -> REPL CommandResult crySession replMode stopOnError =   do settings <- io (setHistoryFile (replSettings isBatch))-     let act = runInputTBehavior behavior settings (withInterrupt (loop 1))+     let act = runInputTBehavior behavior settings (withInterrupt (loop True 1))      if isBatch then asBatch act else act   where   (isBatch,behavior) = case replMode of@@ -63,17 +64,17 @@     Batch path            -> (True,  useFile path)     InteractiveBatch path -> (False, useFile path) -  loop :: Int -> InputT REPL CommandExitCode-  loop lineNum =+  loop :: Bool -> Int -> InputT REPL CommandResult+  loop !success !lineNum =     do ln <- getInputLines =<< MTL.lift getPrompt        case ln of-         NoMoreLines -> return CommandOk+         NoMoreLines -> return emptyCommandResult { crSuccess = success }          Interrupted-           | isBatch && stopOnError -> return CommandError-           | otherwise -> loop lineNum+           | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }+           | otherwise -> loop success lineNum          NextLine ls-           | all (all isSpace) ls -> loop (lineNum + length ls)-           | otherwise            -> doCommand lineNum ls+           | all (all isSpace) ls -> loop success (lineNum + length ls)+           | otherwise            -> doCommand success lineNum ls    run lineNum cmd =     case replMode of@@ -81,16 +82,16 @@       InteractiveBatch _ -> runCommand lineNum Nothing cmd       Batch path         -> runCommand lineNum (Just path) cmd -  doCommand lineNum txt =+  doCommand success lineNum txt =     case parseCommand findCommandExact (unlines txt) of-      Nothing | isBatch && stopOnError -> return CommandError-              | otherwise -> loop (lineNum + length txt)  -- say somtething?+      Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }+              | otherwise -> loop False (lineNum + length txt)  -- say somtething?       Just cmd -> join $ MTL.lift $-        do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd)-           case status of-             CommandError | isBatch && stopOnError -> return (return status)+        do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd)+           case crSuccess status of+             False | isBatch && stopOnError -> return (return status)              _ -> do goOn <- shouldContinue-                     return (if goOn then loop (lineNum + length txt) else return status)+                     return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status)   data NextLine = NextLine [String] | NoMoreLines | Interrupted@@ -107,14 +108,14 @@            | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt            | otherwise -> return $ NextLine $ reverse $ l : ls -loadCryRC :: Cryptolrc -> REPL CommandExitCode+loadCryRC :: Cryptolrc -> REPL CommandResult loadCryRC cryrc =   case cryrc of-    CryrcDisabled   -> return CommandOk+    CryrcDisabled   -> return emptyCommandResult     CryrcDefault    -> check [ getCurrentDirectory, getHomeDirectory ]     CryrcFiles opts -> loadMany opts   where-  check [] = return CommandOk+  check [] = return emptyCommandResult   check (place : others) =     do dir <- io place        let file = dir </> ".cryptolrc"@@ -123,14 +124,14 @@          then crySession (Batch file) True          else check others -  loadMany []       = return CommandOk+  loadMany []       = return emptyCommandResult   loadMany (f : fs) = do status <- crySession (Batch f) True-                         case status of-                           CommandOk -> loadMany fs-                           _         -> return status+                         if crSuccess status+                           then loadMany fs+                           else return status  -- | Haskeline-specific repl implementation.-repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode+repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult repl cryrc replMode callStacks stopOnError begin =   runREPL isBatch callStacks stdoutLogger replAction @@ -143,9 +144,9 @@    replAction =     do status <- loadCryRC cryrc-       case status of-         CommandOk -> begin >> crySession replMode stopOnError-         _         -> return status+       if crSuccess status+         then begin >> crySession replMode stopOnError+         else return status  -- | Try to set the history file. setHistoryFile :: Settings REPL -> IO (Settings REPL)

@@ -9,6 +9,7 @@ module REPL.Logo where  import Cryptol.REPL.Monad+import Cryptol.Utils.Panic (panic) import Paths_cryptol (version)  import Cryptol.Version (commitShortHash,commitDirty)@@ -22,6 +23,7 @@  type Logo = [String] +-- | The list of 'String's returned by the @mk@ function should be non-empty. logo :: Bool -> (String -> [String]) -> Logo logo useColor mk =      [ sgr [SetColor Foreground Dull  White] ++ l | l <- ws ]@@ -43,7 +45,10 @@   slen      = length ls `div` 3   (ws,rest) = splitAt slen ls   (vs,ds)   = splitAt slen rest-  lineLen   = length (head ls)+  line      = case ls of+                line':_ -> line'+                [] -> panic "logo" ["empty lines"]+  lineLen   = length line  displayLogo :: Bool -> Bool -> REPL () displayLogo useColor useUnicode =

@@ -725,16 +725,16 @@ scarry x y = (sx == sy) && (sx != sz)   where     z  = x + y-    sx = x@0-    sy = y@0-    sz = z@0+    sx = head x+    sy = head y+    sz = head z  /**  * Signed borrow.  Returns true if the 2's complement signed subtraction of the  * given bitvector arguments would result in a signed overflow.  */ sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-sborrow x y = ( x <$ (x-y) ) ^ y@0+sborrow x y = ( x <$ (x-y) ) ^ head y  /**  * Zero extension of a bitvector.@@ -747,7 +747,7 @@  */ sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] sext x = newbits # x-  where newbits = if x@0 then ~zero else zero+  where newbits = if head x then ~zero else zero  /**  * 2's complement signed (arithmetic) right shift.  The first argument@@ -850,13 +850,13 @@  * Return the first (left-most) element of a sequence.  */ head : {n, a} [1 + n]a -> a-head xs = xs @ 0+head xs = xs @ (0 : Integer)  /**  * Return the right-most element of a sequence.  */ last : {n, a} (fin n) => [1 + n]a -> a-last xs = xs ! 0+last xs = xs ! (0 : Integer)  /**  * Same as 'split', but with a different type argument order.@@ -985,13 +985,13 @@ sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0   where-    xs' = if `(n/2)  == 1 then xs else sortBy le xs-    ys' = if `(n/^2) == 1 then ys else sortBy le ys+    xs' = if `(n/2)  == (1 : Integer) then xs else sortBy le xs+    ys' = if `(n/^2) == (1 : Integer) then ys else sortBy le ys     zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)              | j == `(n/^2)       then (xs'@i, i+1, j  )              | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )             else                       (ys'@j, i  , j+1)-          | (_, i, j) <- [ (undefined, 0, 0) ] # zs+          | (_, i , j) <- [ (undefined, 0 : Integer, 0 : Integer) ] # zs           ]  // GF_2^n polynomial computations -------------------------------------------

@@ -17,9 +17,9 @@ -- experiments show that it's somewhere under 2^37 at least on 64-bit -- Mac OS X. maxBigIntWidth :: Integer-#if i386_HOST_ARCH+#if defined(i386_HOST_ARCH) maxBigIntWidth = 2^(32 :: Integer) - 0x1-#elif x86_64_HOST_ARCH+#elif defined(x86_64_HOST_ARCH) || defined(aarch64_HOST_ARCH) maxBigIntWidth = 2^(37 :: Integer) - 0x100 #else -- Because GHC doesn't seem to define a CPP macro that will portably

@@ -7,6 +7,8 @@ module Cryptol.Backend.FFI.Error where  import           Control.DeepSeq+import qualified Data.List.NonEmpty as NE+import           Data.List.NonEmpty (NonEmpty) import           GHC.Generics  import           Cryptol.Utils.PP@@ -19,7 +21,7 @@   | CantLoadFFIImpl     String   -- ^ Function name     String   -- ^ Error message-  | FFIDuplicates [Name]+  | FFIDuplicates (NonEmpty Name)   | FFIInFunctor  Name   deriving (Show, Generic, NFData) @@ -38,8 +40,8 @@         --   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)))+           4 (backticks (pp (nameIdent (NE.head xs))) <+>+                 "defined at" <+> align (vcat (map (pp . nameLoc) (NE.toList xs))))       FFIInFunctor x ->         hang (pp (nameLoc x) <.> ":")           4 "Foreign declaration" <+> backticks (pp (nameIdent x)) <+>

@@ -9,9 +9,9 @@   ) where  import           Control.Monad.Writer.Strict-import           Data.Functor-import           Data.Char(isAlphaNum)-import           Data.List+import           Data.Functor                  ((<&>))+import           Data.Char                     (isAlphaNum)+import           Data.List                     (mapAccumL) import           Data.Set                      (Set) import qualified Data.Set                      as Set import           Language.C99.Pretty           as C

@@ -726,7 +726,7 @@ >                      (eitherToE . FP.floatToInteger "trunc" FP.ToZero)) > >   , "roundAway"  ~> unary (roundUnary roundAwayRat->                      (eitherToE . FP.floatToInteger "roundAway" FP.Away))+>                      (eitherToE . FP.floatToInteger "roundAway" FP.NearAway)) > >   , "roundToEven"~> unary (roundUnary round >                      (eitherToE . FP.floatToInteger "roundToEven" FP.NearEven))@@ -1073,6 +1073,7 @@ >   where >    go TVInteger  = pure (VInteger i) >    go TVRational = pure (VRational (fromInteger i))+>    go (TVFloat e p) = pure (VFloat (fpToBF e p (FP.bfFromInteger i))) >    go (TVIntMod n) >         | i < n = pure (VInteger i) >         | otherwise = evalPanic "literal"@@ -1707,13 +1708,23 @@ These functions capture the interactions with rationals.  -This just captures a common pattern for binary floating point primitives.+These just capture common patterns for unary, binary, and ternary floating+point primitives. +> fpUn :: (FP.BFOpts -> BigFloat -> (BigFloat,FP.Status)) ->+>         FP.RoundMode -> Integer -> Integer ->+>         BigFloat -> E BigFloat+> fpUn f r e p x = pure (FP.fpCheckStatus (f (FP.fpOpts e p r) x))+> > fpBin :: (FP.BFOpts -> BigFloat -> BigFloat -> (BigFloat,FP.Status)) -> >          FP.RoundMode -> Integer -> Integer -> >          BigFloat -> BigFloat -> E BigFloat > fpBin f r e p x y = pure (FP.fpCheckStatus (f (FP.fpOpts e p r) x y))-+>+> fpTern :: (FP.BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat,FP.Status)) ->+>           FP.RoundMode -> Integer -> Integer ->+>           BigFloat -> BigFloat -> BigFloat -> E BigFloat+> fpTern f r e p x y z = pure (FP.fpCheckStatus (f (FP.fpOpts e p r) x y z))  Computes the reciprocal of a floating point number via division. This assumes that 1 can be represented exactly, which should be@@ -1752,16 +1763,55 @@ >                           y <- fromVFloat <$> yv >                           pure (VBit (FP.bfCompare x y == EQ)) >->    , "fpIsFinite" ~> vFinPoly \_ -> pure $->                      vFinPoly \_ -> pure $+>    , "fpIsNaN"     ~> vFinPoly \_ -> pure $+>                       vFinPoly \_ -> pure $+>                       VFun \xv ->+>                         do x <- fromVFloat <$> xv+>                            pure (VBit (FP.bfIsNaN x))+>+>    , "fpIsInf"     ~> vFinPoly \_ -> pure $+>                       vFinPoly \_ -> pure $+>                       VFun \xv ->+>                         do x <- fromVFloat <$> xv+>                            pure (VBit (FP.bfIsInf x))+>+>    , "fpIsZero"    ~> vFinPoly \_ -> pure $+>                       vFinPoly \_ -> pure $+>                       VFun \xv ->+>                         do x <- fromVFloat <$> xv+>                            pure (VBit (FP.bfIsZero x))+>+>    , "fpIsNeg"     ~> vFinPoly \_ -> pure $+>                       vFinPoly \_ -> pure $+>                       VFun \xv ->+>                         do x <- fromVFloat <$> xv+>                            pure (VBit (FP.bfIsNeg x))+>+>    , "fpIsNormal"  ~> vFinPoly \e -> pure $+>                       vFinPoly \p -> pure $+>                       VFun \xv ->+>                         do x <- fromVFloat <$> xv+>                            let opts = FP.fpOpts e p fpImplicitRound+>                            pure (VBit (FP.bfIsNormal opts x))+>+>    , "fpIsSubnormal" ~> vFinPoly \e -> pure $+>                         vFinPoly \p -> pure $+>                         VFun \xv ->+>                           do x <- fromVFloat <$> xv+>                              let opts = FP.fpOpts e p fpImplicitRound+>                              pure (VBit (FP.bfIsSubnormal opts x))+>+>    , "fpAdd"      ~> fpBinArith FP.bfAdd+>    , "fpSub"      ~> fpBinArith FP.bfSub+>    , "fpMul"      ~> fpBinArith FP.bfMul+>    , "fpDiv"      ~> fpBinArith FP.bfDiv+>    , "fpFMA"      ~> fpTernArith FP.bfFMA+>    , "fpAbs"      ~> vFinPoly \e -> pure $+>                      vFinPoly \p -> pure $ >                      VFun \xv -> >                        do x <- fromVFloat <$> xv->                           pure (VBit (FP.bfIsFinite x))->->    , "fpAdd"      ~> fpArith FP.bfAdd->    , "fpSub"      ~> fpArith FP.bfSub->    , "fpMul"      ~> fpArith FP.bfMul->    , "fpDiv"      ~> fpArith FP.bfDiv+>                           pure (VFloat (fpToBF e p (FP.bfAbs x)))+>    , "fpSqrt"     ~> fpUnArith FP.bfSqrt > >    , "fpToRational" ~> >       vFinPoly \_ -> pure $@@ -1780,16 +1830,38 @@ >           pure (VFloat (FP.floatFromRational e p rm' rat)) >    ] >   where->   fpArith f = vFinPoly \e -> pure $->               vFinPoly \p -> pure $->               VFun \vr -> pure $->               VFun \xv -> pure $->               VFun \yv ->->                 do r <- fromVWord =<< vr->                    rnd <- eitherToE (FP.fpRound r)->                    x <- fromVFloat <$> xv->                    y <- fromVFloat <$> yv->                    VFloat . fpToBF e p <$> fpBin f rnd e p x y+>   fpUnArith f = vFinPoly \e -> pure $+>                 vFinPoly \p -> pure $+>                 VFun \vr -> pure $+>                 VFun \xv ->+>                   do r <- fromVWord =<< vr+>                      rnd <- eitherToE (FP.fpRound r)+>                      x <- fromVFloat <$> xv+>                      VFloat . fpToBF e p <$> fpUn f rnd e p x+>+>   fpBinArith f = vFinPoly \e -> pure $+>                  vFinPoly \p -> pure $+>                  VFun \vr -> pure $+>                  VFun \xv -> pure $+>                  VFun \yv ->+>                    do r <- fromVWord =<< vr+>                       rnd <- eitherToE (FP.fpRound r)+>                       x <- fromVFloat <$> xv+>                       y <- fromVFloat <$> yv+>                       VFloat . fpToBF e p <$> fpBin f rnd e p x y+>+>   fpTernArith f = vFinPoly \e -> pure $+>                   vFinPoly \p -> pure $+>                   VFun \vr -> pure $+>                   VFun \xv -> pure $+>                   VFun \yv -> pure $+>                   VFun \zv ->+>                     do r <- fromVWord =<< vr+>                        rnd <- eitherToE (FP.fpRound r)+>                        x <- fromVFloat <$> xv+>                        y <- fromVFloat <$> yv+>                        z <- fromVFloat <$> zv+>                        VFloat . fpToBF e p <$> fpTern f rnd e p x y z   Error Handling

@@ -11,6 +11,7 @@ import qualified Data.Map as Map  import Cryptol.TypeCheck.AST+import Cryptol.Utils.Panic ( panic ) import Cryptol.Utils.RecordMap  data Deps = Deps { valDeps  :: Set Name@@ -52,9 +53,10 @@ -- | Compute the transitive closure of the given dependencies. transDeps :: Map Name Deps -> Map Name Deps transDeps mp0 = fst-              $ head+              $ headInfList               $ dropWhile (uncurry (/=))-              $ zip steps (tail steps)+              $ zip steps+              $ drop 1 steps   where   step1 mp d = mconcat [ Map.findWithDefault                             mempty { valDeps = Set.singleton x }@@ -62,6 +64,15 @@   step mp = fmap (step1 mp) mp    steps = iterate step mp0++  -- The only call site for this function is on the result of an invocation+  -- of `iterate`, which returns an infinite list. As such, it is safe to call+  -- `head` on it. Alternatively, we could depend on a library such as+  -- `infinite-list`, but this is likely overkill for this one use site.+  headInfList l =+    case l of+      x:_ -> x+      [] -> panic "transDeps" ["`iterate` returned empty list"]  -- | Dependencies of top-level declarations in a module. -- These are dependencies on module parameters or things

@@ -30,6 +30,9 @@   , getPrimMap   , renameVar   , renameType+  , setFocusedModule+  , Base.renameImpNameInCurrentEnv+  , impNameTopModule      -- * Interfaces   , Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)@@ -45,7 +48,7 @@ import           Cryptol.ModuleSystem.Env import           Cryptol.ModuleSystem.Interface import           Cryptol.ModuleSystem.Monad-import           Cryptol.ModuleSystem.Name (Name,PrimMap)+import           Cryptol.ModuleSystem.Name (Name,PrimMap,nameTopModule) import qualified Cryptol.ModuleSystem.Renamer as R import qualified Cryptol.ModuleSystem.Base as Base import qualified Cryptol.Parser.AST        as P@@ -76,7 +79,7 @@   runModuleM minp{ minpModuleEnv = moduleEnv' } $ do     unloadModule ((InFile path ==) . lmFilePath)     m <- Base.loadModuleByPath True path-    setFocusedModule (T.tcTopEntitytName m)+    setFocusedModule (P.ImpTop (T.tcTopEntitytName m))     return (InFile path,m)  -- | Load the given parsed module.@@ -86,7 +89,7 @@   runModuleM minp{ minpModuleEnv = moduleEnv' } $ do     unloadModule ((n ==) . lmName)     (path,m') <- Base.loadModuleFrom False (FromModule n)-    setFocusedModule (T.tcTopEntitytName m')+    setFocusedModule (P.ImpTop (T.tcTopEntitytName m'))     return (path,m')  -- | Parse and typecheck a module, but don't evaluate or change the environment.@@ -155,3 +158,11 @@ getModuleDependencies :: M.ModName -> ModuleCmd (ModulePath, FileInfo) getModuleDependencies m env = runModuleM env (Base.findDepsOfModule m) +--------------------------------------------------------------------------------+-- ImpName utilities++impNameTopModule :: P.ImpName Name -> M.ModName+impNameTopModule impName =+    case impName of+      P.ImpTop m -> m+      P.ImpNested n -> nameTopModule n

@@ -23,9 +23,12 @@ import Data.Set(Set) import qualified Data.Set as Set import Data.Maybe (fromMaybe)-import Data.List(sortBy,groupBy)+import Data.List(sortBy)+import qualified Data.List.NonEmpty as NE+import Data.List.NonEmpty (NonEmpty(..)) import Data.Function(on) import Data.Monoid ((<>),Endo(..), Any(..))+import qualified Data.Text as T import Data.Text.Encoding (decodeUtf8') import System.Directory (doesFileExist, canonicalizePath) import System.FilePath ( addExtension@@ -67,7 +70,7 @@ 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 +import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards   ( expandPropGuards, runExpandPropGuardsM ) import Cryptol.Parser.NoInclude (removeIncludesModule) import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)@@ -79,7 +82,7 @@  import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName                            , preludeReferenceName, interactiveName, modNameChunks-                           , modNameToNormalModName )+                           , modNameToNormalModName, Namespace(NSModule) ) import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint)@@ -116,6 +119,21 @@ renameModule :: P.Module PName -> ModuleM R.RenamedModule renameModule m = rename (thing (mName m)) mempty (R.renameModule m) +renameImpNameInCurrentEnv :: P.ImpName PName -> ModuleM (P.ImpName Name)+renameImpNameInCurrentEnv (P.ImpTop top) =+ do ok <- isLoaded top+    if ok then+      pure (P.ImpTop top)+    else+      fail ("Top-level module not loaded: " ++ show (pp top))+renameImpNameInCurrentEnv (P.ImpNested pname) =+ do env <- getFocusedEnv+    case R.lookupListNS NSModule pname (mctxNames env) of+      [] -> do+        fail ("Undefined submodule name: " ++ show (pp pname))+      _:_:_ -> do+        fail ("Ambiguous submodule name: " ++ show (pp pname))+      [name] -> pure (P.ImpNested name)  -- NoPat ----------------------------------------------------------------------- @@ -162,7 +180,7 @@                        , "Exception: " ++ show exn ]    txt <- case decodeUtf8' bytes of-    Right txt -> return txt+    Right txt -> return $! (T.replace "\r\n" "\n" txt)     Left e    -> badUtf8 path e    let cfg = P.defaultConfig@@ -320,9 +338,9 @@      where foreigns  = findForeignDecls tcm           foreignFs = T.findForeignDeclsInFunctors tcm-          dups      = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)-                                           $ sortBy (compare `on` nameIdent)-                                           $ map fst foreigns ]+          dups      = [ d | d@(_ :| _ : _) <- NE.groupBy ((==) `on` nameIdent)+                                            $ sortBy (compare `on` nameIdent)+                                            $ map fst foreigns ]           doEvalForeign handleErrs =             case path of               InFile p -> io (loadForeignSrc p) >>=@@ -428,6 +446,7 @@       , iAs      = Nothing       , iSpec    = Nothing       , iInst    = Nothing+      , iDoc     = Nothing       }     } 

@@ -325,7 +325,7 @@       TDNewtype d      -> namingEnv (InModule ns (tlValue d))       TDEnum d         -> namingEnv (InModule ns (tlValue d))       DParamDecl {}    -> mempty-      Include _        -> mempty+      Include {}       -> mempty       DImport {}       -> mempty -- see 'openLoop' in the renamer       DModule m        -> namingEnv (InModule ns (tlValue m))       DModParam {}     -> mempty -- shouldn't happen

@@ -22,14 +22,16 @@  import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc, getForeignSrcPath) import Cryptol.Eval (EvalEnv)+import qualified Cryptol.IR.FreeVars as T import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface-import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)+import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo,nameTopModuleMaybe) import qualified Cryptol.ModuleSystem.NamingEnv as R import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T import qualified Cryptol.TypeCheck.Interface as T import qualified Cryptol.TypeCheck.AST as T+import qualified Cryptol.Utils.Ident as I import Cryptol.Utils.PP (PP(..),text,parens,NameDisp)  import Data.ByteString(ByteString)@@ -82,7 +84,7 @@   -  , meFocusedModule     :: Maybe ModName+  , meFocusedModule     :: Maybe (ImpName Name)     -- ^ The "current" module.  Used to decide how to print names, for example.    , meSearchPath        :: [FilePath]@@ -192,8 +194,8 @@ -- | Try to focus a loaded module in the module environment. focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv focusModule n me = do-  guard (isLoaded n (meLoadedModules me))-  return me { meFocusedModule = Just n }+  guard (isLoaded (ImpTop n) (meLoadedModules me))+  return me { meFocusedModule = Just (ImpTop n) }  -- | Get a list of all the loaded modules. Each module in the -- resulting list depends only on other modules that precede it.@@ -270,10 +272,33 @@                       , mctxNameDisp = R.toNameDisp mempty                       } +findEnv :: Name -> Iface -> T.ModuleG a -> Maybe (R.NamingEnv, Set Name)+findEnv n iface m+  | Just sm <- Map.lookup n (T.mSubmodules m) = Just (T.smInScope sm, ifsPublic (T.smIface sm))+  | Just fn <- Map.lookup n (T.mFunctors m) =+      case Map.lookup n (ifFunctors (ifDefines iface)) of+        Nothing -> panic "findEnv" ["Submodule functor not present in interface"]+        Just d -> Just (T.mInScope fn, ifsPublic (ifNames d))+  | otherwise = asum (fmap (findEnv n iface) (Map.elems (T.mFunctors m))) +modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext+modContextOf (ImpNested name) me =+  do mname <- nameTopModuleMaybe name+     lm <- lookupModule mname me+     (localNames, exported) <- findEnv name (lmInterface lm) (lmModule lm)+     let -- XXX: do we want only public ones here?+         loadedDecls = map (ifDefines . lmInterface)+                     $ getLoadedModules (meLoadedModules me)+     pure ModContext+       { mctxParams   = NoParams+       , mctxExported = exported+       , mctxDecls    = mconcat (ifDefines (lmInterface lm) : loadedDecls)+       , mctxNames    = localNames+       , mctxNameDisp = R.toNameDisp localNames+       }+  -- TODO: support focusing inside a submodule signature to support browsing? -modContextOf :: ModName -> ModuleEnv -> Maybe ModContext-modContextOf mname me =+modContextOf (ImpTop mname) me =   do lm <- lookupModule mname me      let localIface  = lmInterface lm          localNames  = lmNamingEnv lm@@ -467,19 +492,72 @@   -- | Has this module been loaded already.-isLoaded :: ModName -> LoadedModules -> Bool-isLoaded mn lm = mn `Set.member` getLoadedNames lm+isLoaded :: ImpName Name -> LoadedModules -> Bool+isLoaded (ImpTop mn) lm = mn `Set.member` getLoadedNames lm+isLoaded (ImpNested nn) lm = any (check . lmModule) (getLoadedModules lm)+  where+    check :: T.ModuleG a -> Bool+    check m =+      Map.member nn (T.mSubmodules m) ||+      Map.member nn (T.mSignatures m) ||+      Map.member nn (T.mSubmodules m) ||+      any check (T.mFunctors m)  -- | Is this a loaded parameterized module.-isLoadedParamMod :: ModName -> LoadedModules -> Bool-isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln)+isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool+isLoadedParamMod (ImpTop mn) lm = any ((mn ==) . lmName) (lmLoadedParamModules lm)+isLoadedParamMod (ImpNested n) lm =+  any (check1 . lmModule) (lmLoadedModules lm) ||+  any (check2 . lmModule) (lmLoadedParamModules lm)+  where+    -- We haven't crossed into a parameterized functor yet+    check1 m = Map.member n (T.mFunctors m)+            || any check2 (T.mFunctors m) +    -- We're inside a parameterized module and are finished as soon as we have containment+    check2 :: T.ModuleG a -> Bool+    check2 m =+      Map.member n (T.mSubmodules m) ||+      Map.member n (T.mSignatures m) ||+      Map.member n (T.mFunctors m) ||+      any check2 (T.mFunctors m)+ -- | Is this a loaded interface module.-isLoadedInterface :: ModName -> LoadedModules -> Bool-isLoadedInterface mn ln = any ((mn ==) . lmName) (lmLoadedSignatures ln)+isLoadedInterface :: ImpName Name -> LoadedModules -> Bool+isLoadedInterface (ImpTop mn) ln = any ((mn ==) . lmName) (lmLoadedSignatures ln)+isLoadedInterface (ImpNested nn) ln = any (check . lmModule) (getLoadedModules ln)+  where+    check :: T.ModuleG a -> Bool+    check m =+      Map.member nn (T.mSignatures m) ||+      any check (T.mFunctors m) +-- | Return the set of type parameters (@'Set' 'T.TParam'@) and definitions+-- (@'Set' 'Name'@) from the supplied 'LoadedModules' value that another+-- definition (of type @a@) depends on.+loadedParamModDeps ::+  T.FreeVars a =>+  LoadedModules ->+  a ->+  (Set T.TParam, Set Name)+loadedParamModDeps lm a = (badTs, bad)+  where+    ds      = T.freeVars a+    badVals = foldr badName Set.empty (T.valDeps ds)+    bad     = foldr badName badVals (T.tyDeps ds)+    badTs   = T.tyParams ds +    badName nm bs =+      case nameInfo nm of +        -- XXX: Changes if focusing on nested modules+        GlobalName _ I.OrigName { ogModule = I.TopModule m }+          | isLoadedParamMod (ImpTop m) lm -> Set.insert nm bs+          | isLoadedInterface (ImpTop m) lm -> Set.insert nm bs++        _ -> bs++ lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG T.TCTopEntity) lookupTCEntity m env =   case lookupModule m env of@@ -505,7 +583,7 @@   ModName -> T.ModParamNames ->   LoadedModules -> LoadedModules addLoadedSignature path ident fi nameEnv nm si lm-  | isLoaded nm lm = lm+  | isLoaded (ImpTop nm) lm = lm   | otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }   where   loaded = LoadedModule@@ -527,7 +605,7 @@   Maybe ForeignSrc ->   T.Module -> LoadedModules -> LoadedModules addLoadedModule path ident fi nameEnv fsrc tm lm-  | isLoaded (T.mName tm) lm  = lm+  | isLoaded (ImpTop (T.mName tm)) lm  = lm   | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :                                                 lmLoadedParamModules lm }   | otherwise                = lm { lmLoadedModules =

@@ -10,6 +10,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE Safe #-} module Cryptol.ModuleSystem.Interface (     Iface@@ -26,6 +27,7 @@   , filterIfaceDecls   , ifaceDeclsNames   , ifaceOrigNameMap+  , ifaceNameToModuleMap   ) where  import           Data.Set(Set)@@ -45,8 +47,9 @@ import Cryptol.Utils.Ident (ModName, OrigName(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity)-import Cryptol.Parser.AST(Pragma)+import Cryptol.Parser.AST(Pragma, ImpName(..)) import Cryptol.TypeCheck.Type+import Data.Maybe (maybeToList)  type Iface = IfaceG ModName @@ -56,7 +59,7 @@   , ifParams    :: FunctorParams      -- ^ Module parameters, if any   , ifDefines   :: IfaceDecls         -- ^ All things defines in the module                                       -- (includes nested definitions)-  } deriving (Show, Generic, NFData)+  } deriving (Show, Generic, NFData, Functor)  -- | Remove the name of a module.  This is useful for dealing with collections -- of modules, as in `Map (ImpName Name) (IfaceG ())`.@@ -74,8 +77,8 @@   , 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)+  , ifsDoc      :: ![Text]    -- ^ Documentation: more specific to least specific+  } deriving (Show, Generic, NFData, Functor)  -- | Is this interface for a functor. ifaceIsFunctor :: IfaceG name -> Bool@@ -87,7 +90,7 @@                            , ifsDefines = mempty                            , ifsPublic  = mempty                            , ifsNested  = mempty-                           , ifsDoc     = Nothing+                           , ifsDoc     = mempty                            }   , ifParams  = mempty   , ifDefines = mempty@@ -232,9 +235,18 @@                   (concatMap conNames (Map.elems (ifNominalTypes decls)))     where conNames = map fst . nominalTypeConTypes -----+-- | For every name in the interface compute the direct module that defines it.+-- This does not traverse into functors or interfaces.+ifaceNameToModuleMap :: Iface -> Map Name (ImpName Name)+ifaceNameToModuleMap iface = go (ImpTop <$> ifNames iface)+  where+    theModules = ifModules (ifDefines iface) +    go :: IfaceNames (ImpName Name) -> Map Name (ImpName Name)+    go names =+      Map.fromSet (\_ -> ifsName names) (ifsDefines names) <>+      Map.unions+        [ go (ImpNested <$> modu)+        | childName <- Set.toList (ifsNested names)+        , modu <- maybeToList (Map.lookup childName theModules)+        ]

@@ -433,7 +433,7 @@ isLoaded :: P.ModName -> ModuleM Bool isLoaded mn =   do env <- ModuleT get-     pure (MEnv.isLoaded mn (meLoadedModules env))+     pure (MEnv.isLoaded (T.ImpTop mn) (meLoadedModules env))  loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport  = loading . FromImport@@ -577,13 +577,16 @@ getNominalTypes :: ModuleM (Map T.Name T.NominalType) getNominalTypes = ModuleT (loadedNominalTypes <$> get) -getFocusedModule :: ModuleM (Maybe P.ModName)+getFocusedModule :: ModuleM (Maybe (P.ImpName T.Name)) getFocusedModule  = ModuleT (meFocusedModule `fmap` get) -setFocusedModule :: P.ModName -> ModuleM ()-setFocusedModule n = ModuleT $ do+setFocusedModule :: P.ImpName T.Name -> ModuleM ()+setFocusedModule = setMaybeFocusedModule . Just++setMaybeFocusedModule :: Maybe (P.ImpName T.Name) -> ModuleM ()+setMaybeFocusedModule mb = ModuleT $ do   me <- get-  set $! me { meFocusedModule = Just n }+  set $! me { meFocusedModule = mb }  getSearchPath :: ModuleM [FilePath] getSearchPath  = ModuleT (meSearchPath `fmap` get)

@@ -276,7 +276,6 @@ nameTopModule :: Name -> ModName nameTopModule = topModuleFor . nameModPath - -- Name Supply -----------------------------------------------------------------  class Monad m => FreshM m where

@@ -16,6 +16,7 @@ data Names = One Name | Ambig (Set Name) -- ^ Non-empty   deriving (Show,Generic,NFData) +-- | The returned list of names will be non-empty. namesToList :: Names -> [Name] namesToList xs =   case xs of@@ -23,7 +24,14 @@     Ambig ns -> Set.toList ns  anyOne :: Names -> Name-anyOne = head . namesToList+anyOne xs =+  case xs of+    One x -> x+    Ambig ns+      |  Set.null ns+      -> panic "anyOne" ["Ambig with no names"]+      |  otherwise+      -> Set.elemAt 0 ns  instance Semigroup Names where   xs <> ys =

@@ -929,10 +929,14 @@                return (Just n)           Ambig symSet ->             do let syms = Set.toList symSet+                   headSym =+                     case syms of+                       sym:_ -> sym+                       [] -> panic "resolveNameMaybe" ["Ambig with no names"]                mapM_ use syms    -- mark as used to avoid unused warnings                n <- located qn                recordError (MultipleSyms n syms)-               return (Just (head syms))+               return (Just headSym)         Nothing -> pure Nothing @@ -1221,8 +1225,13 @@       (RecordSel a _, RecordSel b _) -> a == b       _                              -> False -  reLoc xs = (head xs) { thing = map thing xs }-+  -- The input comes from UpdField, and as such, it is expected to be a+  -- non-empty list.+  reLoc xs = x { thing = map thing xs }+    where+      x = case xs of+            x':_ -> x'+            [] -> panic "checkLabels" ["UpdFields with no labels"]  mkEInfix :: Expr Name             -- ^ May contain infix expressions          -> (Located Name,Fixity) -- ^ The operator to use

@@ -33,8 +33,9 @@  import Data.List(partition) +import Cryptol.Utils.Ident(identIsNormal, packModName)+import Cryptol.Utils.Panic(panic) import Cryptol.Parser.Position(Range)-import Cryptol.Utils.Ident(packModName) import Cryptol.Parser.AST  {- | Add additional imports for modules nested withing this one -}@@ -56,25 +57,34 @@   processModule :: TopDecl PName -> ([TopDecl PName], [[Ident]])-processModule ~dcl@(DModule m) =-  let NestedModule m1 = tlValue m-  in-  case mDef m1 of-    NormalModule ds ->-      let (childExs, ds1) = addImplicitNestedImports' ds+processModule dcl =+  case dcl of+    DModule m ->+      let NestedModule m1 = tlValue m           mname           = getIdent (thing (mName m1))-          imps            = map (mname :) ([] : childExs) -- this & nested           loc             = srcRange (mName m1)-      in ( DModule m { tlValue = NestedModule m1 { mDef = NormalModule ds1 } }-         : map (mkImp loc) imps-         , case tlExport m of-             Public  -> imps-             Private -> []-         )--    FunctorInstance {} -> ([dcl], [])-    InterfaceModule {} -> ([dcl], [])+      in+      case mDef m1 of+        _ | not (identIsNormal mname) -> ([dcl],[])+        NormalModule ds ->+          let (childExs, ds1) = addImplicitNestedImports' ds+              imps            = map (mname :) ([] : childExs) -- this & nested+          in ( DModule m { tlValue = NestedModule m1 { mDef = NormalModule ds1 } }+             : map (mkImp loc) imps+             , case tlExport m of+                 Public  -> imps+                 Private -> []+             ) +        FunctorInstance {} ->+          let imps = [[mname]]+          in ( dcl : map (mkImp loc) imps+             , case tlExport m of+                 Public  -> imps+                 Private -> []+             )+        InterfaceModule {} -> ([dcl], [])+    _ -> panic "processModule" ["Not a module"]   @@ -107,8 +117,8 @@                      , iAs     = Just (isToQual xs)                      , iSpec   = Nothing                      , iInst   = Nothing+                     , iDoc    = Nothing                      }       }-  

@@ -19,6 +19,7 @@   , parseRepl, parseReplWith   , parseSchema, parseSchemaWith   , parseModName, parseHelpName+  , parseImpName   , ParseError(..), ppError   , Layout(..)   , Config(..), defaultConfig@@ -155,6 +156,7 @@ %name repl    repl %name schema  schema %name modName modName+%name impName impName %name helpName help_name %tokentype { Located Token } %monad { ParseM }@@ -169,7 +171,7 @@   top_module :: { [Module PName] }-  : 'module' module_def       {% mkTopMods $2 }+  : mbDoc 'module' module_def {% mkTopMods $1 $3 }   | 'v{' vmod_body 'v}'       {% mkAnonymousModule $2 }   | 'interface' 'module' modName 'where' 'v{' sig_body 'v}'                               { mkTopSig $3 $6 }@@ -215,10 +217,10 @@   | import                   { [$1] }  -import                          :: { Located (ImportG (ImpName PName)) }-  : 'import' impName optInst mbAs mbImportSpec optImportWhere-                              {% mkImport $1 $2 $3 $4 $5 $6 }-  | 'import' impNameBT mbAs mbImportSpec {% mkBacktickImport $1 $2 $3 $4 }+import                     :: { Located (ImportG (ImpName PName)) }+  : mbDoc 'import' impName optInst mbAs mbImportSpec optImportWhere+                              {% mkImport $2 $3 $4 $5 $6 $7 $1 }+  | mbDoc 'import' impNameBT mbAs mbImportSpec {% mkBacktickImport $2 $3 $4 $5 $1 }  optImportWhere             :: { Maybe (Located [Decl PName]) }   : 'where' whereClause       { Just $2 }@@ -282,7 +284,7 @@ vtop_decl               :: { [TopDecl PName] }   : decl                   { [exportDecl Nothing   Public $1]                 }   | doc decl               { [exportDecl (Just $1) Public $2]                 }-  | mbDoc 'include' STRLIT {% (return . Include) `fmap` fromStrLit $3         }+  | 'include' STRLIT       {% (return . Include) `fmap` fromStrLit $2         }   | mbDoc 'property' name iapats '=' expr                            { [exportDecl $1 Public (mkProperty $3 $4 $6)]     }   | mbDoc 'property' name       '=' expr@@ -294,14 +296,12 @@   | private_decls          { $1                                               }   | mbDoc 'interface' 'constraint' type {% mkInterfaceConstraint $1 $4 }   | parameter_decls        { [ $1 ]                                       }-  | mbDoc 'submodule'-    module_def             {% ((:[]) . exportModule $1) `fmap` mkNested $3 }+  | mbDoc 'submodule' module_def+                           {% ((:[]) . exportModule $1) `fmap` mkNested $3 }    | mbDoc sig_def          { [mkSigDecl $1 $2]  }   | mod_param_decl         { [DModParam $1] }-  | mbDoc import           { [DImport $2] }-    -- we allow for documentation here to avoid conflicts with module paramaters-    -- currently that odcumentation is just discarded+  | import                 { [DImport $1] }   sig_def ::                 { (Located PName, Signature PName) }@@ -331,9 +331,9 @@  private_decls           :: { [TopDecl PName] }   : 'private' 'v{' vtop_decls 'v}'-                           { changeExport Private (reverse $3)                }+                           { changeExport Private (reverse $3) }   | doc 'private' 'v{' vtop_decls 'v}'-                           { changeExport Private (reverse $4)                }+                           {% privateDocedDecl $1 $4 }  prim_bind               :: { [TopDecl PName] }   : mbDoc 'primitive' name  ':' schema       { mkPrimDecl $1 $3 $5 }@@ -343,9 +343,8 @@ foreign_bind            :: { [TopDecl PName] }   : mbDoc 'foreign' name ':' schema          {% mkForeignDecl $1 $3 $5 } -parameter_decls                      :: { TopDecl PName }-  :     'parameter' 'v{' par_decls 'v}' { mkParDecls (reverse $3) }-  | doc 'parameter' 'v{' par_decls 'v}' { mkParDecls (reverse $4) }+parameter_decls         :: { TopDecl PName }+  : 'parameter' 'v{' par_decls 'v}' { mkParDecls (reverse $3) }  -- Reversed par_decls                            :: { [ParamDecl PName] }@@ -357,7 +356,7 @@   : mbDoc        name ':' schema    { mkParFun $1 $2 $4 }   | mbDoc 'type' name ':' kind      {% mkParType $1 $3 $5 }   | mbDoc typeOrPropSyn             { mkIfacePropSyn (thing `fmap` $1) $2 }-  | mbDoc topTypeConstraint         { DParameterConstraint (distrLoc $2) }+  | mbDoc topTypeConstraint         { DParameterConstraint (ParameterConstraint (distrLoc $2) $1) }   doc                     :: { Located Text }@@ -945,6 +944,12 @@ parseModName :: String -> Maybe ModName parseModName txt =   case parseString defaultConfig { cfgModuleScope = False } modName txt of+    Right a -> Just (thing a)+    Left _  -> Nothing++parseImpName :: String -> Maybe (ImpName PName)+parseImpName txt =+  case parseString defaultConfig { cfgModuleScope = False } impName txt of     Right a -> Just (thing a)     Left _  -> Nothing 

@@ -74,6 +74,7 @@   , PrimType(..)   , ParameterType(..)   , ParameterFun(..)+  , ParameterConstraint(..)   , NestedModule(..)   , Signature(..)   , SigDecl(..)@@ -168,6 +169,8 @@     --   Also, for the 'FunctorInstance' case this is not the final result of     --   the names in scope. The typechecker adds in the names in scope in the     --   functor, so this will just contain the names in the enclosing scope.+  , mDocTop   :: Maybe (Located Text)+  -- ^ only used for top-level modules   } deriving (Show, Generic, NFData)  @@ -254,14 +257,14 @@   | DPrimType (TopLevel (PrimType name))   | TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t   | TDEnum (TopLevel (EnumDecl name))   -- ^ @enum T as = cons@-  | Include (Located FilePath)          -- ^ @include File@ (until NoInclude)+  | Include (Located FilePath) -- ^ @include File@ (until NoInclude)    | DParamDecl Range (Signature name)   -- ^ @parameter ...@ (parser only)    | DModule (TopLevel (NestedModule name))      -- ^ @submodule M where ...@   | DImport (Located (ImportG (ImpName name)))  -- ^ @import X@   | DModParam (ModParam name)                   -- ^ @import interface X ...@-  | DInterfaceConstraint (Maybe Text) (Located [Prop name])+  | DInterfaceConstraint (Maybe (Located Text)) (Located [Prop name])     -- ^ @interface constraint@     deriving (Show, Generic, NFData) @@ -276,7 +279,7 @@    | DParameterDecl (SigDecl name)       -- ^ A delcaration in an interface -  | DParameterConstraint [Located (Prop name)]+  | DParameterConstraint (ParameterConstraint name)     -- ^ @parameter type constraint (fin T)@      deriving (Show, Generic, NFData)@@ -359,7 +362,7 @@ data ParameterType name = ParameterType   { ptName    :: Located name     -- ^ name of type parameter   , ptKind    :: Kind             -- ^ kind of parameter-  , ptDoc     :: Maybe Text       -- ^ optional documentation+  , ptDoc     :: Maybe (Located Text) -- ^ optional documentation   , ptFixity  :: Maybe Fixity     -- ^ info for infix use   , ptNumber  :: !Int             -- ^ number of the parameter   } deriving (Eq,Show,Generic,NFData)@@ -368,10 +371,14 @@ data ParameterFun name = ParameterFun   { pfName   :: Located name      -- ^ name of value parameter   , pfSchema :: Schema name       -- ^ schema for parameter-  , pfDoc    :: Maybe Text        -- ^ optional documentation+  , pfDoc    :: Maybe (Located Text) -- ^ optional documentation   , pfFixity :: Maybe Fixity      -- ^ info for infix use   } deriving (Eq,Show,Generic,NFData) +data ParameterConstraint name = ParameterConstraint+  { pcProps  :: [Located (Prop name)] -- ^ constraints+  , pcDoc    :: Maybe (Located Text)  -- ^ optional documentation+  } deriving (Eq,Show,Generic,NFData)  {- | Interface Modules (aka types of functor arguments) @@ -433,6 +440,7 @@   , iSpec      :: Maybe ImportSpec   , iInst      :: !(Maybe (ModuleInstanceArgs PName))     -- ^ `iInst' exists only during parsing+  , iDoc       :: Maybe (Located Text) -- ^ optional documentation   } deriving (Show, Generic, NFData)  type Import = ImportG ModName@@ -483,7 +491,7 @@   , bFixity    :: Maybe Fixity            -- ^ Optional fixity info   , bPragmas   :: [Pragma]                -- ^ Optional pragmas   , bMono      :: Bool                    -- ^ Is this a monomorphic binding-  , bDoc       :: Maybe Text              -- ^ Optional doc string+  , bDoc       :: Maybe (Located Text)    -- ^ Optional doc string   , bExport    :: !ExportType   } deriving (Eq, Generic, NFData, Functor, Show) @@ -828,6 +836,9 @@ instance HasLoc (ParameterFun name) where   getLoc a = getLoc (pfName a) +instance HasLoc (ParameterConstraint name) where+  getLoc a = getLoc (pcProps a)+ instance HasLoc (ModuleG mname name) where   getLoc m     | null locs = Nothing@@ -955,7 +966,7 @@       DPrimType p -> pp p       TDNewtype n -> pp n       TDEnum n -> pp n-      Include l   -> text "include" <+> text (show (thing l))+      Include l -> text "include" <+> text (show (thing l))       DModule d -> pp d       DImport i -> pp (thing i)       DModParam s -> pp s@@ -973,8 +984,7 @@       DParameterFun d -> pp d       DParameterType d -> pp d       DParameterDecl d -> pp d-      DParameterConstraint d ->-        "type constraint" <+> parens (commaSep (map (pp . thing) d))+      DParameterConstraint d -> pp d  ppInterface :: (Show name, PPName name) => Doc -> Signature name -> Doc ppInterface kw sig = kw $$ indent 2 (vcat (is ++ ds))@@ -1029,6 +1039,8 @@   ppPrec _ a = ppPrefixName (pfName a) <+> text ":"                   <+> pp (pfSchema a) +instance (Show name, PPName name) => PP (ParameterConstraint name) where+  ppPrec _ a = "type constraint" <+> parens (commaSep (map (pp . thing) (pcProps a)))  instance (Show name, PPName name) => PP (Decl name) where   ppPrec n decl =@@ -1444,6 +1456,7 @@   noPos m = Module { mName      = mName m                    , mDef       = noPos (mDef m)                    , mInScope   = mInScope m+                   , mDocTop    = noPos (mDocTop m)                    }  instance NoPos (ModuleDefinition name) where@@ -1474,9 +1487,9 @@       DPrimType t -> DPrimType (noPos t)       TDNewtype n -> TDNewtype(noPos n)       TDEnum n -> TDEnum (noPos n)-      Include x   -> Include  (noPos x)+      Include x -> Include (noPos x)       DModule d -> DModule (noPos d)-      DImport d -> DImport (noPos d)+      DImport x -> DImport (noPos x)       DModParam d -> DModParam (noPos d)       DParamDecl _ ds -> DParamDecl rng (noPos ds)         where rng = Range { from = Position 0 0, to = Position 0 0, source = "" }@@ -1508,7 +1521,7 @@   noPos mp = ModParam { mpSignature = noPos (mpSignature mp)                       , mpAs        = mpAs mp                       , mpName      = mpName mp-                      , mpDoc       = noPos <$> mpDoc mp+                      , mpDoc       = mpDoc mp                       , mpRenaming  = mpRenaming mp                       } @@ -1520,6 +1533,9 @@  instance NoPos (ParameterFun x) where   noPos x = x { pfSchema = noPos (pfSchema x) }++instance NoPos (ParameterConstraint x) where+  noPos x = x { pcProps = noPos (pcProps x) }  instance NoPos a => NoPos (TopLevel a) where   noPos tl = tl { tlValue = noPos (tlValue tl) }

@@ -22,6 +22,7 @@ import Cryptol.Parser.AST import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic)+import Data.Foldable (traverse_) import Data.Text (pack) import GHC.Generics (Generic) @@ -31,15 +32,35 @@ runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a runExpandPropGuardsM m = m --- | Error+-- | Errors that can happen while expanding constraint guards. data Error = NoSignature (Located PName)+             -- ^ A declaration using constraints guard lacks an explicit type+             -- signature, which is a requirement.+           | NestedConstraintGuard (Located PName)+             -- ^ Constraint guards appear somewhere other than the top level,+             -- which is not allowed.   deriving (Show, Generic, NFData)  instance PP Error where   ppPrec _ err = case err of     NoSignature x ->-      text "At" <+> pp (srcRange x) <.> colon-        <+> text "Declarations using constraint guards require an explicit type signature."+      hang+        (text "At" <+> pp (srcRange x) <.> colon)+        2+        (vcat [ text "Declaration" <+> backticks (pp (thing x)) <+>+                text "lacks a type signature."+              , text "Declarations using constraint guards require an" <+>+                text "explicit type signature."+              ])+    NestedConstraintGuard x ->+      hang+        (text "At" <+> pp (srcRange x) <.> colon)+        2+        (vcat [ text "Local declaration" <+> backticks (pp (thing x)) <+>+                text "may not use constraint guards."+              , text "Constraint guards may only appear at the top-level of" <+>+                text "a module."+              ])  expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName) expandPropGuards m =@@ -69,16 +90,23 @@ expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName] expandDecl decl =   case decl of-    DBind bind -> do bs <- expandBind bind-                     pure (map DBind bs)-    _          -> pure [decl]+    DBind bind ->+      do bs <- expandBind bind+         pure (map DBind bs)+    DLocated d rng ->+      do ds <- expandDecl d+         pure $ map (`DLocated` rng) ds+    _ ->+      pure [decl]  expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName] expandBind bind =   case thing (bDef bind) of     DImpl (DPropGuards guards) -> expand (DImpl . DPropGuards) guards     DForeign (Just (DPropGuards guards)) -> expand (DForeign . Just . DPropGuards) guards-    _ -> pure [bind]+    _ ->+      do checkNestedGuardsInBind bind+         pure [bind]    where   expand def guards = do@@ -90,6 +118,7 @@           PropGuardCase PName ->           ExpandPropGuardsM (PropGuardCase PName, Bind PName)         goGuard (PropGuardCase props' e) = do+          checkNestedGuardsInExpr e           bName' <- newName (bName bind) (thing <$> props')           -- call to generated function           tParams <- case bSignature bind of@@ -116,6 +145,123 @@     pure $       bind {bDef = def guards' <$ bDef bind} :       binds'++-- | Check for nested uses of constraint guards in an expression (e.g.,+-- in a local definition bound with @where@).+checkNestedGuardsInExpr :: Expr PName -> ExpandPropGuardsM ()+checkNestedGuardsInExpr expr =+  case expr of+    EVar {} ->+      pure ()+    ELit {} ->+      pure ()+    EGenerate e ->+      checkNestedGuardsInExpr e+    ETuple es ->+      traverse_ checkNestedGuardsInExpr es+    ERecord r ->+      traverse_ (checkNestedGuardsInExpr . snd) r+    ESel e _ ->+      checkNestedGuardsInExpr e+    EUpd mbE upds ->+      do traverse_ checkNestedGuardsInExpr mbE+         traverse_ checkNestedGuardsInUpdField upds+    EList es ->+      traverse_ checkNestedGuardsInExpr es+    EFromTo {} ->+      pure ()+    EFromToBy {} ->+      pure ()+    EFromToDownBy {} ->+      pure ()+    EFromToLessThan {} ->+      pure ()+    EInfFrom _ mbE ->+      traverse_ checkNestedGuardsInExpr mbE+    EComp e mss ->+      do checkNestedGuardsInExpr e+         traverse_ (traverse_ checkNestedGuardsInMatch) mss+    EApp e1 e2 ->+      do checkNestedGuardsInExpr e1+         checkNestedGuardsInExpr e2+    EAppT e _ ->+      checkNestedGuardsInExpr e+    EIf e1 e2 e3 ->+      do checkNestedGuardsInExpr e1+         checkNestedGuardsInExpr e2+         checkNestedGuardsInExpr e3+    EWhere e ds ->+      do checkNestedGuardsInExpr e+         traverse_ checkNestedGuardsInDecl ds+    ETyped e _ ->+      checkNestedGuardsInExpr e+    ETypeVal _ ->+      pure ()+    EFun _ _ e ->+      checkNestedGuardsInExpr e+    ELocated e _ ->+      checkNestedGuardsInExpr e+    ESplit e ->+      checkNestedGuardsInExpr e+    EParens e ->+      checkNestedGuardsInExpr e+    EInfix e1 _ _ e2 ->+      do checkNestedGuardsInExpr e1+         checkNestedGuardsInExpr e2+    EPrefix _ e ->+      checkNestedGuardsInExpr e+    ECase e ca ->+      do checkNestedGuardsInExpr e+         traverse_ checkNestedGuardsInCaseAlt ca+  where+    checkNestedGuardsInUpdField :: UpdField PName -> ExpandPropGuardsM ()+    checkNestedGuardsInUpdField (UpdField _ _ e) =+      checkNestedGuardsInExpr e++    checkNestedGuardsInMatch :: Match PName -> ExpandPropGuardsM ()+    checkNestedGuardsInMatch match =+      case match of+        Match _ e ->+          checkNestedGuardsInExpr e+        MatchLet b ->+          checkNestedGuardsInBind b++    checkNestedGuardsInCaseAlt :: CaseAlt PName -> ExpandPropGuardsM ()+    checkNestedGuardsInCaseAlt (CaseAlt _ e) =+      checkNestedGuardsInExpr e++-- | Check for nested uses of constraint guards in a local declaration.+checkNestedGuardsInDecl :: Decl PName -> ExpandPropGuardsM ()+checkNestedGuardsInDecl decl =+  case decl of+    DSignature {} -> pure ()+    DPatBind _ e  -> checkNestedGuardsInExpr e+    DBind b       -> checkNestedGuardsInBind b+    DRec bs       -> traverse_ checkNestedGuardsInBind bs+    DFixity {}    -> pure ()+    DPragma {}    -> pure ()+    DType {}      -> pure ()+    DProp {}      -> pure ()+    DLocated d _  -> checkNestedGuardsInDecl d++-- | Check for nested uses of constraint guards in a local bind.+checkNestedGuardsInBind :: Bind PName -> ExpandPropGuardsM ()+checkNestedGuardsInBind bind =+  case thing (bDef bind) of+    DPrim         -> pure ()+    DImpl bi      -> checkNestedGuardsInBindImpl bi+    DForeign mbBi -> traverse_ checkNestedGuardsInBindImpl mbBi+  where+    nestedConstraintGuards :: ExpandPropGuardsM ()+    nestedConstraintGuards = Left . NestedConstraintGuard $ bName bind++    checkNestedGuardsInBindImpl :: BindImpl PName -> ExpandPropGuardsM ()+    checkNestedGuardsInBindImpl bi =+      case bi of+        DPropGuards _ ->+          nestedConstraintGuards+        DExpr e ->+          checkNestedGuardsInExpr e  patternToExpr :: Pattern PName -> Expr PName patternToExpr (PVar locName) = EVar (thing locName)

@@ -61,13 +61,17 @@ layout isMod ts0    -- Star an implicit layout block at the top of the module-  | let t         = head ts0+  | let t         = case ts0 of+                      t':_ -> t'+                      [] -> panic "layout" ["Unexpected empty list of tokens"]         rng       = srcRange t         blockCol  = max 1 (col (from rng)) -- see startImplicitBlock         implictMod = case map (tokenType . thing) ts0 of-                       KW KW_module : _                   -> False+                       KW KW_module : _ -> False                        KW KW_interface : KW KW_module : _ -> False-                       _                                  -> True+                       White DocStr : KW KW_module : _ -> False+                       White DocStr : KW KW_interface : KW KW_module : _ -> False+                       _ -> True   , isMod && implictMod =     virt rng VCurlyL : go [ Virtual blockCol ] blockCol True ts0 @@ -159,7 +163,11 @@       startImplicitBlock =-      let nextRng  = srcRange (head advanceTokens)+      let curAdvanceTok =+            case advanceTokens of+              curAdvanceTok':_ -> curAdvanceTok'+              [] -> panic "layout" ["Unexpected empty list of advanceTokens"]+          nextRng  = srcRange curAdvanceTok           nextLoc  = from nextRng           blockCol = max 1 (col nextLoc)           -- the `max` ensuraes that indentation is always at least 1,

@@ -342,7 +342,7 @@   do (c,rest) <- T.uncons (input i)      let i' = i { alexPos = move (alexPos i) c, input = rest }          b  = byteForChar c-     return (b,i')+     pure (b, i')  data Layout = Layout | NoLayout 

@@ -563,11 +563,11 @@                           return (Just (thing x))  -checkDocs :: PName -> [Located Text] -> NoPatM (Maybe Text)+checkDocs :: PName -> [Located Text] -> NoPatM (Maybe (Located Text)) checkDocs _ []       = return Nothing-checkDocs _ [d]      = return (Just (thing d))+checkDocs _ [d]      = return (Just d) checkDocs f ds@(d:_) = do recordError $ MultipleDocs f (map srcRange ds)-                          return (Just (thing d))+                          return (Just d)   -- | Does this declaration provide some signatures?

@@ -19,10 +19,9 @@ module Cryptol.Parser.ParserUtils where  import qualified Data.Text as Text-import Data.Char(isAlphaNum)-import Data.Maybe(fromMaybe)+import Data.Char(isAlphaNum, isSpace)+import Data.Maybe(fromMaybe, mapMaybe) import Data.Bits(testBit,setBit)-import Data.Maybe(mapMaybe) import Data.List(foldl') import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.List.NonEmpty as NE@@ -529,7 +528,7 @@             ParamDecl PName mkParFun mbDoc n s = DParameterFun ParameterFun { pfName = n                                                 , pfSchema = s-                                                , pfDoc = thing <$> mbDoc+                                                , pfDoc = mbDoc                                                 , pfFixity = Nothing                                                 } @@ -543,7 +542,7 @@      return (DParameterType              ParameterType { ptName    = n                            , ptKind    = thing k-                           , ptDoc     = thing <$> mbDoc+                           , ptDoc     = mbDoc                            , ptFixity  = Nothing                            , ptNumber  = num                            })@@ -564,6 +563,35 @@       DParamDecl{}            -> decl       DInterfaceConstraint {} -> decl +addDeclDocstring :: Located Text -> TopDecl name -> ParseM (TopDecl name)+addDeclDocstring doc decl =+  case decl of+    Decl d -> Decl  <$> topLevel d+    DPrimType t -> DPrimType <$> topLevel t+    TDNewtype n -> TDNewtype <$> topLevel n+    TDEnum n -> TDEnum <$> topLevel n+    DModule m -> DModule <$> topLevel m+    DModParam p -> pure (DModParam p { mpDoc = Just doc })+    Include _ -> failure "Docstring on include"+    DImport i -> DImport <$> traverse imp i+    DInterfaceConstraint Nothing x -> pure (DInterfaceConstraint (Just doc) x)+    DInterfaceConstraint Just{} _ -> failure "Overlapping docstring"+    DParamDecl{} -> failure "Docstring on parameter declarations"+  where+    failure e = errorMessage (fromMaybe emptyRange (getLoc decl)) [e]+    imp i =+      case iDoc i of+        Nothing -> pure i { iDoc = Just doc }+        Just{}  -> failure "Overlapping docstring"+    topLevel x =+      case tlDoc x of+        Just _ -> failure "Overlapping docstring"+        Nothing -> pure x { tlDoc = Just doc }++privateDocedDecl :: Located Text -> [TopDecl PName] -> ParseM [TopDecl PName]+privateDocedDecl doc (decl:decls) = fmap (: decls) (addDeclDocstring doc decl)+privateDocedDecl doc [] = errorMessage (srcRange doc) ["Docstring on empty private section"]+ mkTypeInst :: Named (Type PName) -> TypeInst PName mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x)              | otherwise                  = NamedInst x@@ -980,39 +1008,67 @@   where    docStr = T.unlines-         $ dropPrefix-         $ trimFront+         $ handlePrefixes          $ T.lines          $ T.dropWhileEnd commentChar          $ thing ltxt    commentChar :: Char -> Bool-  commentChar x = x `elem` ("/* \r\n\t" :: String)--  prefixDroppable x = x `elem` ("* \r\n\t" :: String)+  commentChar x = x `elem` ("/*" :: String) || isSpace x -  whitespaceChar :: Char -> Bool-  whitespaceChar x = x `elem` (" \r\n\t" :: String)+  -- Prefix dropping with a special case for the first line and common+  -- prefix dropping for the following lines. The first line and following+  -- lines are treated independently+  handlePrefixes :: [Text] -> [Text]+  handlePrefixes [] = []+  handlePrefixes (l:ls)+    | T.all commentChar l = ls'+    | otherwise           = T.dropWhile commentChar l : ls'+    where ls' = dropPrefix ls -  trimFront []                     = []-  trimFront (l:ls)-    | T.all commentChar l = ls-    | otherwise           = T.dropWhile commentChar l : ls+  dropPrefix :: [Text] -> [Text]+  dropPrefix ts =+    case startDropPrefixChar ts of+      Nothing -> ts -- done dropping+      Just ts' -> dropPrefix ts' -- keep dropping -  dropPrefix []        = []-  dropPrefix [t]       = [T.dropWhile commentChar t]-  dropPrefix ts@(l:ls) =+  -- At the beginning of a prefix stripping operation we check the+  -- first character of the first line. If that first character is+  -- droppable we use it as the prefix to check for, otherwise we+  -- continue searching for whitespace. Return Nothing if there+  -- was no prefix to drop.+  startDropPrefixChar :: [Text] -> Maybe [Text]+  startDropPrefixChar [] = Nothing+  startDropPrefixChar (l:ls) =     case T.uncons l of-      Just (c,_) | prefixDroppable c &&-                   all (commonPrefix c) ls -> dropPrefix (map (T.drop 1) ts)-      _                                    -> ts+      Nothing -> (l:) <$> searchWhitePrefixChar ls+      Just (c, l')+        | c == '*' || isSpace c -> (l':) <$> checkPrefixChar c ls+        | otherwise -> Nothing -    where-    commonPrefix c t =-      case T.uncons t of-        Just (c',_) -> c == c'-        Nothing     -> whitespaceChar c -- end-of-line matches any whitespace+  -- So far we've only seen empty lines, so we accept empty+  -- lines and lines starting with whitespace.+  searchWhitePrefixChar :: [Text] -> Maybe [Text]+  searchWhitePrefixChar [] = Just []+  searchWhitePrefixChar (l:ls) =+    case T.uncons l of+      Nothing -> (l:) <$> searchWhitePrefixChar ls+      Just (c, l')+        | isSpace c -> (l':) <$> checkPrefixChar c ls+        | otherwise -> Nothing +  -- So far we've seen a non-empty line and we know what character+  -- we're looking for. If that character is whitespace then we also+  -- will accept empty lines as matching the prefix+  checkPrefixChar :: Char -> [Text] -> Maybe [Text]+  checkPrefixChar _ [] = Just []+  checkPrefixChar p (l:ls) =+    case T.uncons l of+      Nothing+        | isSpace p -> (l:) <$> checkPrefixChar p ls+      Just (c,l')+        | c == p -> (l':) <$> checkPrefixChar p ls+      _ -> Nothing  distrLoc :: Located [a] -> [Located a] distrLoc x = [ Located { srcRange = r, thing = a } | a <- thing x ]@@ -1061,6 +1117,7 @@ mkModule nm ds = Module { mName = nm                         , mDef = NormalModule ds                         , mInScope = mempty+                        , mDocTop = Nothing                         }  mkNested :: Module PName -> ParseM (NestedModule PName)@@ -1082,6 +1139,7 @@                         Module { mName    = nm                                , mDef     = InterfaceModule sig                                , mInScope = mempty+                               , mDocTop  = Nothing                                }            } @@ -1089,7 +1147,7 @@   Maybe (Located Text) -> Type PName -> ParseM [TopDecl PName] mkInterfaceConstraint mbDoc ty =   do ps <- mkProp ty-     pure [DInterfaceConstraint (thing <$> mbDoc) ps]+     pure [DInterfaceConstraint mbDoc ps]  mkParDecls :: [ParamDecl PName] -> TopDecl PName mkParDecls ds = DParamDecl loc (mkInterface' [] ds)@@ -1122,7 +1180,7 @@   add s d =     case d of       DParameterType pt       -> s { sigTypeParams  = pt  : sigTypeParams s  }-      DParameterConstraint ps -> s { sigConstraints = ps ++ sigConstraints s }+      DParameterConstraint ps -> s { sigConstraints = pcProps ps ++ sigConstraints s }       DParameterDecl pd       -> s { sigDecls       = pd  : sigDecls s       }       DParameterFun pf        -> s { sigFunParams   = pf  : sigFunParams s   } @@ -1145,7 +1203,7 @@  -- | Make an unnamed module---gets the name @Main@. mkAnonymousModule :: [TopDecl PName] -> ParseM [Module PName]-mkAnonymousModule = mkTopMods+mkAnonymousModule = mkTopMods Nothing                   . mkModule Located { srcRange = emptyRange                                      , thing    = mkModName [T.pack "Main"]                                      }@@ -1159,6 +1217,7 @@   Module { mName    = nm          , mDef     = FunctorInstance fun (DefaultInstAnonArg ds) mempty          , mInScope = mempty+         , mDocTop  = Nothing          }  mkModuleInstance ::@@ -1170,6 +1229,7 @@   Module { mName    = m          , mDef     = FunctorInstance f as emptyModuleInstance          , mInScope = mempty+         , mDocTop  = Nothing          }  @@ -1178,9 +1238,15 @@   case (h,ls) of     (UpdSet, [l]) | RecordSel i Nothing <- thing l ->       pure Named { name = l { thing = i }, value = e }-    _ -> errorMessage (srcRange (head ls))+    _ -> errorMessage (srcRange lab)             ["Invalid record field.  Perhaps you meant to update a record?"]+  where+    -- The list of field updates in an UpdField should always be non-empty.+    lab = case ls of+            lab':_ -> lab'+            [] -> panic "ufToNamed" ["UpdField with empty labels"] +-- | The returned list of 'Selector's will be non-empty. exprToFieldPath :: Expr PName -> ParseM [Located Selector] exprToFieldPath e0 = reverse <$> go noLoc e0   where@@ -1190,7 +1256,11 @@       ELocated e1 r -> go r e1       ESel e2 s ->         do ls <- go loc e2-           let rng = loc { from = to (srcRange (head ls)) }+           let l =+                 case ls of+                   l':_ -> l'+                   [] -> panic "exprToFieldPath" ["empty list of selectors"]+           let rng = loc { from = to (srcRange l) }            pure (Located { thing = s, srcRange = rng } : ls)       EVar (UnQual l) ->         pure [ Located { thing = RecordSel l Nothing, srcRange = loc } ]@@ -1230,6 +1300,7 @@   Located (ImpName PName) ->   Maybe (Located ModName) ->   Maybe (Located ImportSpec) ->+  Maybe (Located Text) ->   ParseM (Located (ImportG (ImpName PName))) mkBacktickImport loc impName mbAs mbImportSpec =   mkImport loc impName (Just inst) mbAs mbImportSpec Nothing@@ -1244,9 +1315,10 @@   Maybe (Located ModName) ->   Maybe (Located ImportSpec) ->   Maybe (Located [Decl PName]) ->+  Maybe (Located Text) ->   ParseM (Located (ImportG (ImpName PName))) -mkImport loc impName optInst mbAs mbImportSpec optImportWhere =+mkImport loc impName optInst mbAs mbImportSpec optImportWhere doc =   do i <- getInst      let end = fromMaybe (srcRange impName)              $ msum [ srcRange <$> optImportWhere@@ -1260,6 +1332,7 @@                                  , iAs        = thing <$> mbAs                                  , iSpec      = thing <$> mbImportSpec                                  , iInst      = i+                                 , iDoc       = doc                                  }                   }   where@@ -1286,14 +1359,17 @@   -mkTopMods :: Module PName -> ParseM [Module PName]-mkTopMods = desugarMod+mkTopMods :: Maybe (Located Text) -> Module PName -> ParseM [Module PName]+mkTopMods doc m =+ do (m', ms) <- desugarMod m { mDocTop = doc }+    pure (ms ++ [m'])  mkTopSig :: Located ModName -> Signature PName -> [Module PName] mkTopSig nm sig =   [ Module { mName    = nm            , mDef     = InterfaceModule sig            , mInScope = mempty+           , mDocTop  = Nothing            }   ] @@ -1318,8 +1394,9 @@                 . getIdent   toImpName     = ImpNested --desugarMod :: MkAnon name => ModuleG name PName -> ParseM [ModuleG name PName]+-- | Desugar a module returning first the updated original module and a+-- list of any new modules generated by desugaring.+desugarMod :: MkAnon name => ModuleG name PName -> ParseM (ModuleG name PName, [ModuleG name PName]) desugarMod mo =   case mDef mo of @@ -1337,16 +1414,20 @@          let i      = mkAnon AnonArg (thing (mName mo))              nm     = Located { srcRange = srcRange (mName mo), thing = i }              as'    = DefaultInstArg (ModuleArg . toImpName <$> nm)-         pure [ Module-                  { mName = nm, mDef  = NormalModule lds', mInScope = mempty }-              , mo { mDef = FunctorInstance f as' mempty }-              ]+         pure ( mo { mDef = FunctorInstance f as' mempty }+              , [ Module+                    { mName = nm+                    , mDef  = NormalModule lds'+                    , mInScope = mempty+                    , mDocTop = Nothing+                    }]+              )      NormalModule ds ->       do (newMs, newDs) <- desugarTopDs (mName mo) ds-         pure (newMs ++ [ mo { mDef = NormalModule newDs } ])+         pure (mo {mDef = NormalModule newDs }, newMs) -    _ -> pure [mo]+    _ -> pure (mo, [])   desugarTopDs ::@@ -1389,6 +1470,7 @@              pure ( [ Module { mName = nm                              , mDef = InterfaceModule sig                              , mInScope = mempty+                             , mDocTop = Nothing                              }                      ]                   , [ DModParam@@ -1410,19 +1492,27 @@         in         case d of -          DImport i | ImpTop _ <- iModule (thing i)-                    , Nothing  <- iInst (thing i) ->+          DImport i+            | ImpTop _ <- iModule (thing i)+            , Nothing  <- iInst (thing i) ->             cont [d] (addI i sig) -          DImport i | Just inst <- iInst (thing i) ->+          DImport i+            | Just inst <- iInst (thing i) ->             do newDs <- desugarInstImport i inst                cont newDs sig            DParamDecl _ ds' -> cont [] (jnSig ds' sig)            DModule tl | NestedModule mo <- tlValue tl ->-            do ms <- desugarMod mo-               cont [ DModule tl { tlValue = NestedModule m } | m <- ms ] sig+            do (mo', ms) <- desugarMod mo+               cont ([ DModule TopLevel+                          { tlExport = tlExport tl+                          , tlValue = NestedModule m+                          , tlDoc = Nothing -- generated modules have no docstrings+                          }+                      | m <- ms] ++ [DModule tl { tlValue = NestedModule mo' }])+                    sig            _ -> cont [d] sig @@ -1431,17 +1521,19 @@   ModuleInstanceArgs PName          {- ^ The insantiation -} ->   ParseM [TopDecl PName] desugarInstImport i inst =-  do ms <- desugarMod+  do (m, ms) <- desugarMod            Module { mName    = i { thing = iname }                   , mDef     = FunctorInstance                                  (iModule <$> i) inst emptyModuleInstance                   , mInScope = mempty+                  , mDocTop  = Nothing                   }-     pure (DImport (newImp <$> i) : map modTop ms)+     pure (DImport (newImp <$> i) : map modTop (ms ++ [m]))    where   imp = thing i   iname = mkUnqual+        $ identAnonIfaceMod         $ mkIdent         $ "import of " <> nm <> " at " <> Text.pack (show (pp (srcRange i)))     where

@@ -81,13 +81,13 @@   where   comment current []    = mk Comment current   comment current (l : ls)-    | Just op <- isOpenFence l = mk Comment (l : current) ++ fenced op [] ls+    | Just (fence, op) <- isOpenFence l = mk Comment (l : current) ++ fenced fence op [] ls     | isBlank l         = blanks (l : current) ls     | otherwise         = comment (l : current) ls    blanks current []     = mk Comment current   blanks current (l : ls)-    | Just op <- isOpenFence l = mk Comment (l : current) ++ fenced op [] ls+    | Just (fence, op) <- isOpenFence l = mk Comment (l : current) ++ fenced fence op [] ls     | isCodeLine l             = mk Comment current ++ code [l] ls     | isBlank l                = blanks  (l : current) ls     | otherwise                = comment (l : current) ls@@ -97,24 +97,39 @@     | isCodeLine l      = code (l : current) ls     | otherwise         = mk Code current ++ comment [] (l : ls) -  fenced op current []     = mk op current  -- XXX should this be an error?-  fenced op current (l : ls)-    | isCloseFence l    = mk op current ++ comment [l] ls-    | otherwise         = fenced op (l : current) ls+  fenced _ op current [] = mk op current  -- XXX should this be an error?+  fenced fence op current (l : ls)+    | isCloseFence fence l = mk op current ++ comment [l] ls+    | otherwise         = fenced fence op (l : current) ls     isOpenFence l-    | "```" `Text.isPrefixOf` l' =-      Just $ case Text.dropWhile isSpace (Text.drop 3 l') of-               l'' | "cryptol" `Text.isPrefixOf` l'' -> Code-                   | isBlank l''                     -> Code-                   | otherwise                       -> Comment+    | (spaces, l1) <- Text.span (' ' ==) l+    , (ticks,  l2) <- Text.span('`' ==) l1+    , 3 <= Text.length ticks+    , not (Text.elem '`' l2)+    , let info = Text.strip l2+    , let n = Text.length spaces+    = Just (Text.length ticks, case info of+              "cryptol" -> Code . map (trimIndent n)+              ""        -> Code . map (trimIndent n)+              _         -> Comment)      | otherwise = Nothing     where-    l' = Text.dropWhile isSpace l+      trimIndent n t =+        case Text.span (' ' ==) t of+          (prefix, suffix)+            | Text.length prefix <= n -> suffix+            | otherwise -> Text.drop n prefix <> suffix+  +  isCloseFence fence l =+    fence <= Text.length ticks &&+    Text.all (' ' ==) l2+    where+      l1 = Text.dropWhile (' ' ==) l+      (ticks, l2) = Text.span ('`' ==) l1 -  isCloseFence l = "```" `Text.isPrefixOf` Text.dropWhile isSpace l   isBlank l      = Text.all isSpace l   isCodeLine l   = "\t" `Text.isPrefixOf` l || "    " `Text.isPrefixOf` l 

@@ -8,10 +8,9 @@ -- -- Compile the prelude into the executable as a last resort -{-# LANGUAGE Safe #-} {-# LANGUAGE CPP #-}-{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}  module Cryptol.Prelude   ( preludeContents@@ -23,28 +22,27 @@   , cryptolTcContents   ) where -import Data.ByteString(ByteString)+import Data.ByteString (ByteString)+import Data.FileEmbed (embedFileRelative) import qualified Data.ByteString.Char8 as B-import Text.Heredoc (there) - preludeContents :: ByteString-preludeContents = B.pack [there|lib/Cryptol.cry|]+preludeContents = $(embedFileRelative "lib/Cryptol.cry")  preludeReferenceContents :: ByteString-preludeReferenceContents = B.pack [there|lib/Cryptol/Reference.cry|]+preludeReferenceContents = $(embedFileRelative "lib/Cryptol/Reference.cry")  floatContents :: ByteString-floatContents = B.pack [there|lib/Float.cry|]+floatContents = $(embedFileRelative "lib/Float.cry")  arrayContents :: ByteString-arrayContents = B.pack [there|lib/Array.cry|]+arrayContents = $(embedFileRelative "lib/Array.cry")  suiteBContents :: ByteString-suiteBContents = B.pack [there|lib/SuiteB.cry|]+suiteBContents = $(embedFileRelative "lib/SuiteB.cry")  primeECContents :: ByteString-primeECContents = B.pack [there|lib/PrimeEC.cry|]+primeECContents = $(embedFileRelative "lib/PrimeEC.cry")  cryptolTcContents :: String-cryptolTcContents = [there|lib/CryptolTC.z3|]+cryptolTcContents = B.unpack $(embedFileRelative "lib/CryptolTC.z3")

@@ -202,13 +202,13 @@ ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_sub p s t = ec_add p s u   where u = case BN.bigNatSub (primeMod p) (py t) of-              (# | y' #)    -> t{ py = y' }+              (# | y' #)    -> t{ py = y' `BN.bigNatRem` (primeMod p) }               (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))] {-# INLINE ec_sub #-}   ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint-ec_negate p s = s{ py = BN.bigNatSubUnsafe (primeMod p) (py s) }+ec_negate p s = s{ py = (BN.bigNatSubUnsafe (primeMod p) (py s))  `BN.bigNatRem` (primeMod p) } {-# INLINE ec_negate #-}  -- | Compute the elliptic curve group addition operation@@ -294,7 +294,7 @@   | BN.bigNatIsZero (pz s) = zro   | otherwise =       case m of-        0# -> panic "ec_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))]+        0# -> panic "ec_mult" ["integer with 0 width", show h]         _  -> go m zro   where

@@ -18,7 +18,7 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.REPL.Command (     -- * Commands-    Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)+    Command(..), CommandDescr(..), CommandBody(..), CommandResult(..)   , parseCommand   , runCommand   , splitCommand@@ -26,6 +26,7 @@   , findCommandExact   , findNbCommand   , commandList+  , emptyCommandResult    , moduleCmd, loadCmd, loadPrelude, setOptionCmd @@ -45,6 +46,11 @@   , onlineProveSat   , offlineProveSat +    -- Check docstrings+  , checkDocStrings+  , SubcommandResult(..)+  , DocstringResult(..)+     -- Misc utilities   , handleCtrlC   , sanitize@@ -62,6 +68,8 @@ import Cryptol.REPL.Help  import qualified Cryptol.ModuleSystem as M+import qualified Cryptol.ModuleSystem.Interface as M+import qualified Cryptol.ModuleSystem.Monad as M import qualified Cryptol.ModuleSystem.Name as M import qualified Cryptol.ModuleSystem.NamingEnv as M import qualified Cryptol.ModuleSystem.Renamer as M@@ -73,7 +81,7 @@ import           Cryptol.Backend.FloatHelpers as FP import qualified Cryptol.Backend.Monad as E import qualified Cryptol.Backend.SeqMap as E-import           Cryptol.Eval.Concrete( Concrete(..) )+import Cryptol.Backend.Concrete ( Concrete(..) ) import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Env as E import           Cryptol.Eval.FFI@@ -85,7 +93,7 @@ import qualified Cryptol.Testing.Random  as TestR import Cryptol.Parser     (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig-    ,parseModName,parseHelpName)+    ,parseModName,parseHelpName,parseImpName) import           Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..)) import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.Error as T@@ -138,7 +146,7 @@ import qualified System.Random.TF.Instances as TFI import Numeric (showFFloat) import qualified Data.Text as T-import Data.IORef(newIORef,readIORef,writeIORef)+import Data.IORef(newIORef, readIORef, writeIORef, modifyIORef)  import GHC.Float (log1p, expm1) @@ -146,6 +154,7 @@ import Prelude.Compat  import qualified Data.SBV.Internals as SBV (showTDiff)+import Data.Foldable (foldl')   @@ -153,7 +162,7 @@  -- | Commands. data Command-  = Command (Int -> Maybe FilePath -> REPL ())         -- ^ Successfully parsed command+  = Command (Int -> Maybe FilePath -> REPL CommandResult) -- ^ Successfully parsed command   | Ambiguous String [String] -- ^ Ambiguous command, list of conflicting                               --   commands   | Unknown String            -- ^ The unknown command@@ -177,21 +186,30 @@   compare = compare `on` cNames  data CommandBody-  = ExprArg     (String   -> (Int,Int) -> Maybe FilePath -> REPL ())-  | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ())-  | DeclsArg    (String   -> REPL ())-  | ExprTypeArg (String   -> REPL ())-  | ModNameArg  (String   -> REPL ())-  | FilenameArg (FilePath -> REPL ())-  | OptionArg   (String   -> REPL ())-  | ShellArg    (String   -> REPL ())-  | HelpArg     (String   -> REPL ())-  | NoArg       (REPL ())-+  = ExprArg     (String   -> (Int,Int) -> Maybe FilePath -> REPL CommandResult)+  | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult)+  | DeclsArg    (String   -> REPL CommandResult)+  | ExprTypeArg (String   -> REPL CommandResult)+  | ModNameArg  (String   -> REPL CommandResult)+  | FilenameArg (FilePath -> REPL CommandResult)+  | OptionArg   (String   -> REPL CommandResult)+  | ShellArg    (String   -> REPL CommandResult)+  | HelpArg     (String   -> REPL CommandResult)+  | NoArg       (REPL CommandResult) -data CommandExitCode = CommandOk-                     | CommandError -- XXX: More?+data CommandResult = CommandResult+  { crType :: Maybe String -- ^ type output for relevant commands+  , crValue :: Maybe String -- ^ value output for relevant commands+  , crSuccess :: Bool -- ^ indicator that command successfully performed its task+  }+  deriving (Show) +emptyCommandResult :: CommandResult+emptyCommandResult = CommandResult+  { crType = Nothing+  , crValue = Nothing+  , crSuccess = True+  }  -- | REPL command parsing. commands :: CommandMap@@ -260,7 +278,7 @@   , CommandDescr [ ":ast" ] ["EXPR"] (ExprArg astOfCmd)     "Print out the pre-typechecked AST of a given term."     ""-  , CommandDescr [ ":extract-coq" ] [] (NoArg allTerms)+  , CommandDescr [ ":extract-coq" ] [] (NoArg extractCoqCmd)     "Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."     ""   , CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd)@@ -290,6 +308,9 @@   , CommandDescr [ ":new-seed"] [] (NoArg newSeedCmd)       "Randomly generate and set a new seed for the random number generator"       ""+  , CommandDescr [ ":check-docstrings" ] [] (ModNameArg checkDocStringsCmd)+      "Run the REPL code blocks in the module's docstring comments"+      ""   ]  commandList :: [CommandDescr]@@ -316,6 +337,9 @@   , CommandDescr [ ":m", ":module" ] ["[ MODULE ]"] (FilenameArg moduleCmd)     "Load a module by its name."     ""+  , CommandDescr [ ":f", ":focus" ] ["[ MODULE ]"] (ModNameArg focusCmd)+    "Focus name scope inside a loaded module."+    ""   , CommandDescr [ ":w", ":writeByteArray" ] ["FILE", "EXPR"] (FileExprArg writeFileCmd)     "Write data of type 'fin n => [n][8]' to a file."     ""@@ -361,23 +385,27 @@ -- Command Evaluation ----------------------------------------------------------  -- | Run a command.-runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode+runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandResult runCommand lineNum mbBatch c = case c of -  Command cmd -> (cmd lineNum mbBatch >> return CommandOk) `Cryptol.REPL.Monad.catch` handler+  Command cmd -> cmd lineNum mbBatch `Cryptol.REPL.Monad.catch` handler     where-    handler re = rPutStrLn "" >> rPrint (pp re) >> return CommandError+    handler re = do+      rPutStrLn ""+      rPrint (pp re)+      return emptyCommandResult { crSuccess = False } -  Unknown cmd -> do rPutStrLn ("Unknown command: " ++ cmd)-                    return CommandError+  Unknown cmd -> do+    rPutStrLn ("Unknown command: " ++ cmd)+    return emptyCommandResult { crSuccess = False }    Ambiguous cmd cmds -> do     rPutStrLn (cmd ++ " is ambiguous, it could mean one of:")     rPutStrLn ("\t" ++ intercalate ", " cmds)-    return CommandError+    return emptyCommandResult { crSuccess = False }  -evalCmd :: String -> Int -> Maybe FilePath -> REPL ()+evalCmd :: String -> Int -> Maybe FilePath -> REPL CommandResult evalCmd str lineNum mbBatch = do   ri <- replParseInput str lineNum mbBatch   case ri of@@ -393,15 +421,26 @@       --out <- io $ rethrowEvalError       --          $ return $!! show $ pp $ E.WithBase ppOpts val -      rPutStrLn (show valDoc)+      let value = show valDoc+      rPutStrLn value+      pure emptyCommandResult { crValue = Just value }+     P.LetInput ds -> do       -- explicitly make this a top-level declaration, so that it will       -- be generalized if mono-binds is enabled       replEvalDecls ds+      pure emptyCommandResult+     P.EmptyInput ->       -- comment or empty input does nothing-      pure ()+      pure emptyCommandResult +  -- parsing and evaluating expressions can fail in many different ways+  `catch` \e -> do+      rPutStrLn ""+      rPrint (pp e)+      pure emptyCommandResult { crSuccess = False }+ printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL () printCounterexample cexTy exprDoc vs =   do ppOpts <- getPPValOpts@@ -421,7 +460,7 @@      rPrint $ nest 2 (sep ([exprDoc] ++ docs ++ [text "= True"]))  -dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()+dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult dumpTestsCmd outFile str pos fnm =   do expr <- replParseExpr str pos fnm      (val, ty) <- replEvalExpr expr@@ -439,11 +478,12 @@               do argOut <- mapM (rEval . E.ppValue Concrete ppopts) args                  resOut <- rEval (E.ppValue Concrete ppopts x)                  return (renderOneLine resOut ++ "\t" ++ intercalate "\t" (map renderOneLine argOut) ++ "\n")-     io $ writeFile outFile (concat out) `X.catch` handler-  where-    handler :: X.SomeException -> IO ()-    handler e = putStrLn (X.displayException e)-+     writeResult <- io $ X.try (writeFile outFile (concat out))+     case writeResult of+       Right{} -> pure emptyCommandResult+       Left e ->+         do rPutStrLn (X.displayException (e :: X.SomeException))+            pure emptyCommandResult { crSuccess = False }   data QCMode = QCRandom | QCExhaust deriving (Eq, Show)@@ -452,27 +492,34 @@ -- | Randomly test a property, or exhaustively check it if the number -- of values in the type under test is smaller than the @tests@ -- environment variable, or we specify exhaustive testing.-qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL ()+qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult qcCmd qcMode "" _pos _fnm =   do (xs,disp) <- getPropertyNames      let nameStr x = show (fixNameDisp disp (pp x))      if null xs-        then rPutStrLn "There are no properties in scope."-        else forM_ xs $ \(x,d) ->+        then do+          rPutStrLn "There are no properties in scope."+          pure emptyCommandResult { crSuccess = False }+        else do+          let evalProp result (x,d) =                do let str = nameStr x                   rPutStr $ "property " ++ str ++ " "                   let texpr = T.EVar x                   let schema = M.ifDeclSig d                   nd <- M.mctxNameDisp <$> getFocusedEnv                   let doc = fixNameDisp nd (pp texpr)-                  void (qcExpr qcMode doc texpr schema)+                  testReport <- qcExpr qcMode doc texpr schema+                  pure $! result && isPass (reportResult testReport)+          success <- foldM evalProp True xs+          pure emptyCommandResult { crSuccess = success }  qcCmd qcMode str pos fnm =   do expr <- replParseExpr str pos fnm      (_,texpr,schema) <- replCheckExpr expr      nd <- M.mctxNameDisp <$> getFocusedEnv      let doc = fixNameDisp nd (ppPrec 3 expr) -- function application has precedence 3-     void (qcExpr qcMode doc texpr schema)+     testReport <- qcExpr qcMode doc texpr schema+     pure emptyCommandResult { crSuccess = isPass (reportResult testReport) }   data TestReport = TestReport@@ -492,14 +539,14 @@   do (val,ty) <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of        Just res -> pure res        -- If instance is not found, doesn't necessarily mean that there is no instance.-       -- And due to nondeterminism in result from the solver (for finding solution to +       -- And due to nondeterminism in result from the solver (for finding solution to        -- numeric type constraints), `:check` can get to this exception sometimes, but        -- successfully find an instance and test with it other times.        Nothing -> raise (InstantiationsNotFound schema)      testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"      tenv <- E.envTypes . M.deEnv <$> getDynEnv      let tyv = E.evalValType tenv ty-     -- tv has already had polymorphism instantiated +     -- tv has already had polymorphism instantiated      percentRef <- io $ newIORef Nothing      testsRef <- io $ newIORef 0 @@ -687,7 +734,7 @@     proportion = negate (expm1 (numD * log1p (negate (recip szD)))) -satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult satCmd = cmdProveSat True proveCmd = cmdProveSat False @@ -709,7 +756,7 @@       ]  -- | Attempts to prove the given term is safe for all inputs-safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult safeCmd str pos fnm = do   proverName <- getKnownUser "prover"   fileName   <- getKnownUser "smtFile"@@ -722,16 +769,21 @@   (_,texpr,schema) <- replCheckExpr pexpr    if proverName `elem` ["offline","sbv-offline","w4-offline"] then-    offlineProveSat proverName SafetyQuery texpr schema mfile+    do success <- offlineProveSat proverName SafetyQuery texpr schema mfile+       pure emptyCommandResult { crSuccess = success }   else      do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery texpr schema mfile)-        case result of+        cmdResult <- case result of           EmptyResult         ->             panic "REPL.Command" [ "got EmptyResult for online prover query" ] -          ProverError msg -> rPutStrLn msg+          ProverError msg ->+            do rPutStrLn msg+               pure emptyCommandResult { crSuccess = False } -          ThmResult _ts -> rPutStrLn "Safe"+          ThmResult _ts ->+            do rPutStrLn "Safe"+               pure emptyCommandResult            CounterExample cexType tevs -> do             rPutStrLn "Counterexample"@@ -746,41 +798,52 @@              void $ bindItVariable t e +            pure emptyCommandResult { crSuccess = False }+           AllSatResult _ -> do             panic "REPL.Command" ["Unexpected AllSAtResult for ':safe' call"]          seeStats <- getUserShowProverStats         when seeStats (showProverStats firstProver stats)+        pure cmdResult   -- | Console-specific version of 'proveSat'. Prints output to the -- console, and binds the @it@ variable to a record whose form depends -- on the expression given. See ticket #66 for a discussion of this -- design.-cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL ()+cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult cmdProveSat isSat "" _pos _fnm =   do (xs,disp) <- getPropertyNames      let nameStr x = show (fixNameDisp disp (pp x))      if null xs-        then rPutStrLn "There are no properties in scope."-        else forM_ xs $ \(x,d) ->-               do let str = nameStr x-                  if isSat-                     then rPutStr $ ":sat "   ++ str ++ "\n\t"-                     else rPutStr $ ":prove " ++ str ++ "\n\t"-                  let texpr = T.EVar x-                  let schema = M.ifDeclSig d-                  nd <- M.mctxNameDisp <$> getFocusedEnv-                  let doc = fixNameDisp nd (pp texpr)-                  proveSatExpr isSat (M.nameLoc x) doc texpr schema+        then do+          rPutStrLn "There are no properties in scope."+          pure emptyCommandResult { crSuccess = False }+        else do+          let check acc (x,d) = do+                let str = nameStr x+                if isSat+                  then rPutStr $ ":sat "   ++ str ++ "\n\t"+                  else rPutStr $ ":prove " ++ str ++ "\n\t"+                let texpr = T.EVar x+                let schema = M.ifDeclSig d+                nd <- M.mctxNameDisp <$> getFocusedEnv+                let doc = fixNameDisp nd (pp texpr)+                success <- proveSatExpr isSat (M.nameLoc x) doc texpr schema+                pure $! acc && success+          success <- foldM check True xs+          pure emptyCommandResult { crSuccess = success } + cmdProveSat isSat str pos fnm = do   pexpr <- replParseExpr str pos fnm   nd <- M.mctxNameDisp <$> getFocusedEnv   let doc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3   (_,texpr,schema) <- replCheckExpr pexpr   let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr)-  proveSatExpr isSat rng doc texpr schema+  success <- proveSatExpr isSat rng doc texpr schema+  pure emptyCommandResult { crSuccess = success }  proveSatExpr ::   Bool ->@@ -788,7 +851,7 @@   Doc ->   T.Expr ->   T.Schema ->-  REPL ()+  REPL Bool proveSatExpr isSat rng exprDoc texpr schema = do   let cexStr | isSat = "satisfying assignment"              | otherwise = "counterexample"@@ -801,16 +864,17 @@      offlineProveSat proverName qtype texpr schema mfile   else      do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName qtype texpr schema mfile)-        case result of+        success <- case result of           EmptyResult         ->             panic "REPL.Command" [ "got EmptyResult for online prover query" ] -          ProverError msg     -> rPutStrLn msg+          ProverError msg -> False <$ rPutStrLn msg -          ThmResult ts        -> do+          ThmResult ts -> do             rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")             (t, e) <- mkSolverResult cexStr rng (not isSat) (Left ts)             void $ bindItVariable t e+            pure (not isSat)            CounterExample cexType tevs -> do             rPutStrLn "Counterexample"@@ -829,6 +893,7 @@               _ -> return ()              void $ bindItVariable t e+            pure False            AllSatResult tevss -> do             rPutStrLn "Satisfiable"@@ -859,14 +924,17 @@               [e] -> void $ bindItVariable ty e               _   -> bindItVariables ty exprs +            pure True+         seeStats <- getUserShowProverStats         when seeStats (showProverStats firstProver stats)+        pure success   printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL () printSafetyViolation texpr schema vs =     catch-      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of +      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of             Just (fn, _) -> pure fn             Nothing -> raise (EvalPolyError schema)           rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs))@@ -889,6 +957,7 @@   decls <- fmap M.deDecls getDynEnv   timing <- io (newIORef 0)   ~(EnvBool ignoreSafety) <- getUser "ignoreSafety"+  ~(EnvNum timeoutSec) <- getUser "proverTimeout"   let cmd = ProverCommand {           pcQueryType    = qtype         , pcProverName   = proverName@@ -902,16 +971,16 @@         , pcIgnoreSafety = ignoreSafety         }   (firstProver, res) <- getProverConfig >>= \case-       Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd+       Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg timeoutSec cmd        Right w4Cfg ->          do ~(EnvBool hashConsing) <- getUser "hashConsing"             ~(EnvBool warnUninterp) <- getUser "warnUninterp"-            liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd+            liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp timeoutSec cmd    stas <- io (readIORef timing)   return (firstProver,res,stas) -offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL ()+offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL Bool offlineProveSat proverName qtype expr schema mfile = do   verbose <- getKnownUser "debug"   modelValidate <- getUserProverValidate@@ -950,12 +1019,13 @@     Left sbvCfg ->       do result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd          case result of-           Left msg -> rPutStrLn msg+           Left msg -> False <$ rPutStrLn msg            Right smtlib -> do              io $ displayMsg              case mfile of                Just path -> io $ writeFile path smtlib                Nothing -> rPutStr smtlib+             pure True      Right _w4Cfg ->       do ~(EnvBool hashConsing) <- getUser "hashConsing"@@ -974,6 +1044,7 @@          case result of            Just msg -> rPutStrLn msg            Nothing -> return ()+         pure True   rIdent :: M.Ident@@ -1010,7 +1081,7 @@       let argName = M.packIdent ("arg" ++ show n)        in ((argName,t),(argName,e)) -specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult specializeCmd str pos fnm = do   parseExpr <- replParseExpr str pos fnm   (_, expr, schema) <- replCheckExpr parseExpr@@ -1020,9 +1091,11 @@   rPutStrLn  "Original expression:"   rPutStrLn $ dump expr   rPutStrLn  "Specialized expression:"-  rPutStrLn $ dump spexpr+  let value = dump spexpr+  rPutStrLn value+  pure emptyCommandResult { crValue = Just value } -refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult refEvalCmd str pos fnm = do   parseExpr <- replParseExpr str pos fnm   (_, expr, schema) <- replCheckExpr parseExpr@@ -1030,20 +1103,24 @@   validEvalContext schema   val <- liftModuleCmd (rethrowEvalError . R.evaluate expr)   opts <- getPPValOpts-  rPrint $ R.ppEValue opts val+  let value = show (R.ppEValue opts val)+  rPutStrLn value+  pure emptyCommandResult { crValue = Just value } -astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult astOfCmd str pos fnm = do  expr <- replParseExpr str pos fnm  (re,_,_) <- replCheckExpr (P.noPos expr)  rPrint (fmap M.nameUnique re)+ pure emptyCommandResult -allTerms :: REPL ()-allTerms = do+extractCoqCmd :: REPL CommandResult+extractCoqCmd = do   me <- getModuleEnv   rPrint $ T.showParseable $ concatMap T.mDecls $ M.loadedModules me+  pure emptyCommandResult -typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()+typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult typeOfCmd str pos fnm = do    expr         <- replParseExpr str pos fnm@@ -1053,10 +1130,13 @@   whenDebug (rPutStrLn (dump def))   fDisp <- M.mctxNameDisp <$> getFocusedEnv   -- type annotation ':' has precedence 2-  rPrint $ runDoc fDisp $ group $ hang-    (ppPrec 2 expr <+> text ":") 2 (pp sig)+  let output = show $ runDoc fDisp $ group $ hang+                 (ppPrec 2 expr <+> text ":") 2 (pp sig) -timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()+  rPutStrLn output+  pure emptyCommandResult { crType = Just output }++timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult timeCmd str pos fnm = do   period <- getKnownUser "timeMeasurementPeriod" :: REPL Int   quiet <- getKnownUser "timeQuiet"@@ -1081,12 +1161,13 @@             (pure $ E.VFloat $ FP.floatFromDouble benchAvgCpuTime)             (pure $ E.VInteger $ toInteger benchAvgCycles)       bindItVariableVal itType itVal+  pure emptyCommandResult -- TODO: gather timing outputs -readFileCmd :: FilePath -> REPL ()+readFileCmd :: FilePath -> REPL CommandResult readFileCmd fp = do   bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)   case bytes of-    Nothing -> return ()+    Nothing -> return emptyCommandResult { crSuccess = False }     Just bs ->       do pm <- getPrimMap          let val = byteStringToInteger bs@@ -1098,6 +1179,7 @@          let x = T.EProofApp (T.ETApp (T.ETApp number (T.tNum val)) t)          let expr = T.EApp f x          void $ bindItVariable (E.TVSeq (toInteger len) (E.TVSeq 8 E.TVBit)) expr+         pure emptyCommandResult  -- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer' -- with @8*n@ bits. This function uses a balanced binary fold to@@ -1118,16 +1200,19 @@     x1 = byteStringToInteger bs1     x2 = byteStringToInteger bs2 -writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()+writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult writeFileCmd file str pos fnm = do   expr         <- replParseExpr str pos fnm   (val,ty)     <- replEvalExpr expr   if not (tIsByteSeq ty)-   then rPrint $  "Cannot write expression of types other than [n][8]."+    then do+      rPrint $ "Cannot write expression of types other than [n][8]."               <+> "Type was: " <+> pp ty-   else wf file =<< serializeValue val+      pure emptyCommandResult { crSuccess = False }+    else do+      bytes <- serializeValue val+      replWriteFile file bytes  where-  wf fp bytes = replWriteFile fp bytes (rPutStrLn . show)   tIsByteSeq x = maybe False                        (tIsByte . snd)                        (T.tIsSeq x)@@ -1150,32 +1235,36 @@ rEvalRethrow :: E.Eval a -> REPL a rEvalRethrow m = io $ rethrowEvalError $ E.runEval mempty m -reloadCmd :: REPL ()+reloadCmd :: REPL CommandResult reloadCmd  = do   mb <- getLoadedMod   case mb of     Just lm  ->       case lPath lm of         M.InFile f -> loadCmd f-        _ -> return ()-    Nothing -> return ()+        _ -> return emptyCommandResult+    Nothing -> return emptyCommandResult  -editCmd :: String -> REPL ()+editCmd :: String -> REPL CommandResult editCmd path =   do mbE <- getEditPath      mbL <- getLoadedMod      if not (null path)         then do when (isNothing mbL)-                  $ setLoadedMod LoadedModule { lName = Nothing+                  $ setLoadedMod LoadedModule { lFocus = Nothing                                               , lPath = M.InFile path }                 doEdit path         else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of-               Nothing -> rPutStrLn "No filed to edit."+               Nothing ->+                do rPutStrLn "No filed to edit."+                   pure emptyCommandResult { crSuccess = False }                Just p  ->                   case p of                     M.InFile f   -> doEdit f-                    M.InMem l bs -> withROTempFile l bs replEdit >> pure ()+                    M.InMem l bs -> do+                      _ <- withROTempFile l bs replEdit+                      pure emptyCommandResult   where   doEdit p =     do setEditPath p@@ -1213,9 +1302,9 @@   -moduleCmd :: String -> REPL ()+moduleCmd :: String -> REPL CommandResult moduleCmd modString-  | null modString = return ()+  | null modString = return emptyCommandResult   | otherwise      = do     case parseModName modString of       Just m ->@@ -1223,33 +1312,71 @@            case mpath of              M.InFile file ->                do setEditPath file-                  setLoadedMod LoadedModule { lName = Just m, lPath = mpath }+                  setLoadedMod LoadedModule { lFocus = Just (P.ImpTop m), lPath = mpath }                   loadHelper (M.loadModuleByPath file)              M.InMem {} -> loadHelper (M.loadModuleByName m)-      Nothing -> rPutStrLn "Invalid module name."+      Nothing ->+        do rPutStrLn "Invalid module name."+           pure emptyCommandResult { crSuccess = False } ++focusCmd :: String -> REPL CommandResult+focusCmd modString+  | null modString =+   do mb <- getLoadedMod+      case mb of+        Nothing -> pure ()+        Just lm ->+          case lName lm of+            Nothing -> pure ()+            Just name -> do+              let top = P.ImpTop name+              liftModuleCmd (`M.runModuleM` M.setFocusedModule top)+              setLoadedMod lm { lFocus = Just top }+      pure emptyCommandResult++  | otherwise =+    case parseImpName modString of+      Nothing ->+        do rPutStrLn "Invalid module name."+           pure emptyCommandResult { crSuccess = False }+    +      Just pimpName -> do+        impName <- liftModuleCmd (setFocusedModuleCmd pimpName)+        mb <- getLoadedMod+        case mb of+          Nothing -> pure ()+          Just lm -> setLoadedMod lm { lFocus = Just impName }+        pure emptyCommandResult++setFocusedModuleCmd :: P.ImpName P.PName -> M.ModuleCmd (P.ImpName T.Name)+setFocusedModuleCmd pimpName i = M.runModuleM i $+ do impName <- M.renameImpNameInCurrentEnv pimpName+    M.setFocusedModule impName+    pure impName+ loadPrelude :: REPL ()-loadPrelude  = moduleCmd $ show $ pp M.preludeName+loadPrelude  = void $ moduleCmd $ show $ pp M.preludeName -loadCmd :: FilePath -> REPL ()+loadCmd :: FilePath -> REPL CommandResult loadCmd path-  | null path = return ()+  | null path = return emptyCommandResult    -- when `:load`, the edit and focused paths become the parameter   | otherwise = do setEditPath path-                   setLoadedMod LoadedModule { lName = Nothing+                   setLoadedMod LoadedModule { lFocus = Nothing                                              , lPath = M.InFile path                                              }                    loadHelper (M.loadModuleByPath path) -loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL ()+loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL CommandResult loadHelper how =   do clearLoadedMod      (path,ent) <- liftModuleCmd how       whenDebug (rPutStrLn (dump ent))      setLoadedMod LoadedModule-        { lName = Just (T.tcTopEntitytName ent)+        { lFocus = Just (P.ImpTop (T.tcTopEntitytName ent))         , lPath = path         }      -- after a successful load, the current module becomes the edit target@@ -1257,51 +1384,68 @@        M.InFile f -> setEditPath f        M.InMem {} -> clearEditPath      setDynEnv mempty+     pure emptyCommandResult -genHeaderCmd :: FilePath -> REPL ()+genHeaderCmd :: FilePath -> REPL CommandResult genHeaderCmd path-  | null path = pure ()+  | null path = pure emptyCommandResult   | otherwise = do     (mPath, m) <- liftModuleCmd $ M.checkModuleByPath path     let decls = case m of                    T.TCTopModule mo -> findForeignDecls mo                    T.TCTopSignature {} -> []     if null decls-      then rPutStrLn $ "No foreign declarations in " ++ pretty mPath+      then do+        rPutStrLn $ "No foreign declarations in " ++ pretty mPath+        pure emptyCommandResult { crSuccess = False }       else do         let header = generateForeignHeader decls         case mPath of           M.InFile p -> do             let hPath = p -<.> "h"             rPutStrLn $ "Writing header to " ++ hPath-            replWriteFileString hPath header (rPutStrLn . show)-          M.InMem _ _ -> rPutStrLn header+            replWriteFileString hPath header+          M.InMem _ _ ->+            do rPutStrLn header+               pure emptyCommandResult -versionCmd :: REPL ()-versionCmd = displayVersion rPutStrLn+versionCmd :: REPL CommandResult+versionCmd = do+  displayVersion rPutStrLn+  pure emptyCommandResult -quitCmd :: REPL ()-quitCmd  = stop+quitCmd :: REPL CommandResult+quitCmd  = do+  stop+  pure emptyCommandResult -browseCmd :: String -> REPL ()+browseCmd :: String -> REPL CommandResult browseCmd input   | null input =     do fe <- getFocusedEnv        rPrint (browseModContext BrowseInScope fe)+       pure emptyCommandResult   | otherwise =-    case parseModName input of-      Nothing -> rPutStrLn "Invalid module name"-      Just m ->-        do mb <- M.modContextOf m <$> getModuleEnv-           case mb of-             Nothing -> rPutStrLn ("Module " ++ show input ++ " is not loaded")-             Just fe -> rPrint (browseModContext BrowseExported fe)+    case parseImpName input of+      Nothing -> do+        rPutStrLn "Invalid module name"+        pure emptyCommandResult { crSuccess = False }+      Just pimpName -> do+        impName <- liftModuleCmd (`M.runModuleM` M.renameImpNameInCurrentEnv pimpName)+        mb <- M.modContextOf impName <$> getModuleEnv+        case mb of+          Nothing -> do+            rPutStrLn ("Module " ++ show input ++ " is not loaded")+            pure emptyCommandResult { crSuccess = False }+          Just fe -> do+            rPrint (browseModContext BrowseExported fe)+            pure emptyCommandResult  -setOptionCmd :: String -> REPL ()+setOptionCmd :: String -> REPL CommandResult setOptionCmd str-  | Just value <- mbValue = setUser key value-  | null key              = mapM_ (describe . optName) (leaves userOptions)+  | Just value <- mbValue = setUser key value >>= \success -> pure emptyCommandResult { crSuccess = success }+  | null key              = mapM_ (describe . optName) (leaves userOptions) >> pure emptyCommandResult   | otherwise             = describe key   where   (before,after) = break (== '=') str@@ -1313,11 +1457,13 @@   describe k = do     ev <- tryGetUser k     case ev of-      Just v  -> rPutStrLn (k ++ " = " ++ showEnvVal v)+      Just v  -> do rPutStrLn (k ++ " = " ++ showEnvVal v)+                    pure emptyCommandResult       Nothing -> do rPutStrLn ("Unknown user option: `" ++ k ++ "`")                     when (any isSpace k) $ do                       let (k1, k2) = break isSpace k                       rPutStrLn ("Did you mean: `:set " ++ k1 ++ " =" ++ k2 ++ "`?")+                    pure emptyCommandResult { crSuccess = False }  showEnvVal :: EnvVal -> String showEnvVal ev =@@ -1329,29 +1475,33 @@     EnvBool False -> "off"  -- XXX at the moment, this can only look at declarations.-helpCmd :: String -> REPL ()+helpCmd :: String -> REPL CommandResult helpCmd cmd-  | null cmd  = mapM_ rPutStrLn (genHelp commandList)+  | null cmd  = emptyCommandResult <$ mapM_ rPutStrLn (genHelp commandList)   | cmd0 : args <- words cmd, ":" `isPrefixOf` cmd0 =     case findCommandExact cmd0 of-      []  -> void $ runCommand 1 Nothing (Unknown cmd0)+      []  -> runCommand 1 Nothing (Unknown cmd0)       [c] -> showCmdHelp c args-      cs  -> void $ runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs))+      cs  -> runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs))   | otherwise =+    wrapResult <$>     case parseHelpName cmd of-      Just qname -> helpForNamed qname-      Nothing    -> rPutStrLn ("Unable to parse name: " ++ cmd)+      Just qname -> True <$ helpForNamed qname+      Nothing    -> False <$ rPutStrLn ("Unable to parse name: " ++ cmd)    where-  showCmdHelp c [arg] | ":set" `elem` cNames c = showOptionHelp arg+  wrapResult success = emptyCommandResult { crSuccess = success }++  showCmdHelp c [arg] | ":set" `elem` cNames c = wrapResult <$> showOptionHelp arg   showCmdHelp c _args =     do rPutStrLn ("\n    " ++ intercalate ", " (cNames c) ++ " " ++ intercalate " " (cArgs c))        rPutStrLn ""        rPutStrLn (cHelp c)        rPutStrLn ""-       when (not (null (cLongHelp c))) $ do+       unless (null (cLongHelp c)) $ do          rPutStrLn (cLongHelp c)          rPutStrLn ""+       pure emptyCommandResult    showOptionHelp arg =     case lookupTrieExact arg userOptions of@@ -1364,22 +1514,24 @@            rPutStrLn ""            rPutStrLn (optHelp opt)            rPutStrLn ""-      [] -> rPutStrLn ("Unknown setting name `" ++ arg ++ "`")-      _  -> rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`")+           pure True+      [] -> False <$ rPutStrLn ("Unknown setting name `" ++ arg ++ "`")+      _  -> False <$ rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`")  -runShellCmd :: String -> REPL ()+runShellCmd :: String -> REPL CommandResult runShellCmd cmd   = io $ do h <- Process.runCommand cmd             _ <- waitForProcess h-            return ()+            return emptyCommandResult -- This could check for exit code 0 -cdCmd :: FilePath -> REPL ()-cdCmd f | null f = rPutStrLn $ "[error] :cd requires a path argument"+cdCmd :: FilePath -> REPL CommandResult+cdCmd f | null f = do rPutStrLn $ "[error] :cd requires a path argument"+                      pure emptyCommandResult { crSuccess = False }         | otherwise = do   exists <- io $ doesDirectoryExist f   if exists-    then io $ setCurrentDirectory f+    then emptyCommandResult <$ io (setCurrentDirectory f)     else raise $ DirectoryNotFound f  -- C-c Handlings ---------------------------------------------------------------@@ -1472,12 +1624,12 @@        -- ignore certain warnings during typechecking       filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning-      filterTypecheck (M.TypeCheckWarnings nameMap xs) = -        case filter (allow . snd) xs of +      filterTypecheck (M.TypeCheckWarnings nameMap xs) =+        case filter (allow . snd) xs of           [] -> Nothing           ys -> Just (M.TypeCheckWarnings nameMap ys)           where-            allow :: T.Warning -> Bool +            allow :: T.Warning -> Bool             allow = \case               T.DefaultingTo _ _ | not warnDefaulting -> False               T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False@@ -1587,17 +1739,21 @@ itIdent :: M.Ident itIdent  = M.packIdent "it" -replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL ()+replWriteFile :: FilePath -> BS.ByteString -> REPL CommandResult replWriteFile = replWriteFileWith BS.writeFile -replWriteFileString :: FilePath -> String -> (X.SomeException -> REPL ()) -> REPL ()+replWriteFileString :: FilePath -> String -> REPL CommandResult replWriteFileString = replWriteFileWith writeFile -replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a ->-  (X.SomeException -> REPL ()) -> REPL ()-replWriteFileWith write fp contents handler =- do x <- io $ X.catch (write fp contents >> return Nothing) (return . Just)-    maybe (return ()) handler x+replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a -> REPL CommandResult+replWriteFileWith write fp contents =+ do x <- io (X.try (write fp contents))+    case x of+      Left e ->+        do rPutStrLn (show (e :: X.SomeException))+           pure emptyCommandResult { crSuccess = False }+      Right _ ->+        pure emptyCommandResult  replReadFile :: FilePath -> (X.SomeException -> REPL (Maybe BS.ByteString)) -> REPL (Maybe BS.ByteString) replReadFile fp handler =@@ -1670,11 +1826,13 @@  type CommandMap = Trie CommandDescr -newSeedCmd :: REPL ()+newSeedCmd :: REPL CommandResult newSeedCmd =   do  seed <- createAndSetSeed       rPutStrLn "Seed initialized to:"-      rPutStrLn (show seed)+      let value = show seed+      rPutStrLn value+      pure emptyCommandResult { crValue = Just value }   where     createAndSetSeed =       withRandomGen $ \g0 ->@@ -1685,11 +1843,12 @@             seed = (s1, s2, s3, s4)         in  pure (seed, TF.seedTFGen seed) -seedCmd :: String -> REPL ()+seedCmd :: String -> REPL CommandResult seedCmd s =-  case mbGen of-    Nothing -> rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers."-    Just gen -> setRandomGen gen+  do success <- case mbGen of+       Nothing -> False <$ rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers."+       Just gen -> True <$ setRandomGen gen+     pure emptyCommandResult { crSuccess = success }    where     mbGen =@@ -1797,13 +1956,14 @@   -moduleInfoCmd :: Bool -> String -> REPL ()+moduleInfoCmd :: Bool -> String -> REPL CommandResult moduleInfoCmd isFile name   | isFile = showInfo =<< liftModuleCmd (M.getFileDependencies name)   | otherwise =     case parseModName name of       Just m  -> showInfo =<< liftModuleCmd (M.getModuleDependencies m)-      Nothing -> rPutStrLn "Invalid module name."+      Nothing -> do rPutStrLn "Invalid module name."+                    pure emptyCommandResult { crSuccess = False }    where   showInfo (p,fi) =@@ -1830,6 +1990,235 @@        depList show               "foreign"  (Map.toList (M.fiForeignDeps fi))         rPutStrLn "}"+       pure emptyCommandResult +-- | Extract the code blocks from the body of a docstring.+--+-- A single code block starts with at least 3 backticks followed by an+-- optional language specifier of "cryptol". This allowed other kinds+-- of code blocks to be included (and ignored) in docstrings. Longer+-- backtick sequences can be used when a code block needs to be able to+-- contain backtick sequences.+--+-- @+-- /**+--  * A docstring example+--  *+--  * ```cryptol+--  * :check example+--  * ```+--  */+-- @+extractCodeBlocks :: T.Text -> [[T.Text]]+extractCodeBlocks raw = go [] (T.lines raw)+  where+    go finished [] = reverse finished+    go finished (x:xs)+      | (spaces, x1) <- T.span (' ' ==) x+      , (ticks, x2) <- T.span ('`' ==) x1+      , 3 <= T.length ticks+      , not (T.elem '`' x2)+      , let info = T.strip x2+      = if info `elem` ["", "repl"] -- supported languages "unlabeled" and repl+        then keep finished (T.length spaces) (T.length ticks) [] xs+        else skip finished ticks xs+      | otherwise = go finished xs +    -- process a code block that we're keeping+    keep finished _ _ acc [] = go (reverse acc : finished) [] -- unterminated code fences are defined to be terminated by github+    keep finished indentLen ticksLen acc (x:xs)+      | x1 <- T.dropWhile (' ' ==) x+      , (ticks, x2) <- T.span ('`' ==) x1+      , ticksLen <= T.length ticks+      , T.all (' ' ==) x2+      = go (reverse acc : finished) xs +      | otherwise =+        let x' =+              case T.span (' ' ==) x of+                (spaces, x1)+                  | T.length spaces <= indentLen -> x1+                  | otherwise -> T.drop indentLen x+        in keep finished indentLen ticksLen (x' : acc) xs++    -- process a code block that we're skipping+    skip finished _ [] = go finished []+    skip finished close (x:xs)+      | close == x = go finished xs+      | otherwise = skip finished close xs++data SubcommandResult = SubcommandResult+  { srInput :: T.Text+  , srResult :: CommandResult+  , srLog :: String+  }++-- | Check a single code block from inside a docstring.+--+-- The result will contain the results of processing the commands up to+-- the first failure.+--+-- Execution of the commands is run in an isolated REPL environment.+checkBlock ::+  [T.Text] {- ^ lines of the code block -} ->+  REPL [SubcommandResult]+checkBlock = isolated . go+  where+    go [] = pure []+    go (line:block) =+      case parseCommand (findNbCommand True) (T.unpack line) of+        Nothing -> do+          pure [SubcommandResult+            { srInput = line+            , srLog = "Failed to parse command"+            , srResult = emptyCommandResult { crSuccess = False }+            }]+        Just Ambiguous{} -> do+          pure [SubcommandResult+            { srInput = line+            , srLog = "Ambiguous command"+            , srResult = emptyCommandResult { crSuccess = False }+            }]+        Just Unknown{} -> do+          pure [SubcommandResult+            { srInput = line+            , srLog = "Unknown command"+            , srResult = emptyCommandResult { crSuccess = False }+            }]+        Just (Command cmd) -> do+          (logtxt, eresult) <- captureLog (Cryptol.REPL.Monad.try (cmd 0 Nothing))+          case eresult of+            Left e -> do+              let result = SubcommandResult+                    { srInput = line+                    , srLog = logtxt ++ show (pp e) ++ "\n"+                    , srResult = emptyCommandResult { crSuccess = False }+                    }+              pure [result]+            Right result -> do+              let subresult = SubcommandResult+                    { srInput = line+                    , srLog = logtxt+                    , srResult = result+                    }+              subresults <- checkBlock block+              pure (subresult : subresults)++captureLog :: REPL a -> REPL (String, a)+captureLog m = do+  previousLogger <- getLogger+  outputsRef <- io (newIORef [])+  setPutStr (\str -> modifyIORef outputsRef (str:))+  result <- m `finally` setLogger previousLogger+  outputs <- io (readIORef outputsRef)+  let output = interpretControls (concat (reverse outputs))+  pure (output, result)++-- | Apply control character semantics to the result of the logger+interpretControls :: String -> String+interpretControls ('\b' : xs) = interpretControls xs+interpretControls (_ : '\b' : xs) = interpretControls xs+interpretControls (x : xs) = x : interpretControls xs+interpretControls [] = []++-- | The result of running a docstring as attached to a definition+data DocstringResult = DocstringResult+  { drName   :: T.DocFor -- ^ The associated definition of the docstring+  , drFences :: [[SubcommandResult]] -- ^ list of fences in this definition's docstring+  }++-- | Check all the code blocks in a given docstring.+checkDocItem :: T.DocItem -> REPL DocstringResult+checkDocItem item =+ do xs <- case traverse extractCodeBlocks (T.docText item) of+            [] -> pure [] -- optimization+            bs ->+              Ex.bracket+                (liftModuleCmd (`M.runModuleM` (M.getFocusedModule <* M.setFocusedModule (T.docModContext item))))+                (\mb -> liftModuleCmd (`M.runModuleM` M.setMaybeFocusedModule mb))+                (\_ -> traverse checkBlock (concat bs))+    pure DocstringResult+      { drName = T.docFor item+      , drFences = xs+      }++-- | Check all of the docstrings in the given module.+--+-- The outer list elements correspond to the code blocks from the+-- docstrings in file order. Each inner list corresponds to the+-- REPL commands inside each of the docstrings.+checkDocStrings :: M.LoadedModule -> REPL [DocstringResult]+checkDocStrings m = do+  let dat = M.lmdModule (M.lmData m)+  let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat+  traverse checkDocItem ds++-- | Evaluate all the docstrings in the specified module.+--+-- This command succeeds when:+-- * the module can be found+-- * the docstrings can be parsed for code blocks+-- * all of the commands in the docstrings succeed+checkDocStringsCmd ::+  String {- ^ module name -} ->+  REPL CommandResult+checkDocStringsCmd input+  | null input = do+    mb <- getLoadedMod+    case lName =<< mb of+      Nothing -> do+        rPutStrLn "No current module"+        pure emptyCommandResult { crSuccess = False }+      Just mn -> checkModName mn+  | otherwise =+    case parseModName input of+      Nothing -> do+        rPutStrLn "Invalid module name"+        pure emptyCommandResult { crSuccess = False }+      Just mn -> checkModName mn++  where++    countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)+    countOutcomes = foldl' countOutcomes1 (0, 0, 0)+      where+        countOutcomes1 (successes, nofences, failures) []+          = (successes, nofences + 1, failures)+        countOutcomes1 acc result = foldl' countOutcomes2 acc result++        countOutcomes2 (successes, nofences, failures) result+          | crSuccess (srResult result) = (successes + 1, nofences, failures)+          | otherwise = (successes, nofences, failures + 1)+++    checkModName :: P.ModName -> REPL CommandResult+    checkModName mn = do+        mb <- M.lookupModule mn <$> getModuleEnv+        case mb of+          Nothing -> do+            rPutStrLn ("Module " ++ show input ++ " is not loaded")+            pure emptyCommandResult { crSuccess = False }++          Just fe+            | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do+              rPutStrLn "Skipping docstrings on parameterized module"+              pure emptyCommandResult++            | otherwise -> do+              results <- checkDocStrings fe+              let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]++              forM_ results $ \dr ->+                unless (null (drFences dr)) $+                 do rPutStrLn ""+                    rPutStrLn ("\nChecking " ++ show (pp (drName dr)))+                    forM_ (drFences dr) $ \fence ->+                      forM_ fence $ \line -> do+                        rPutStrLn ""+                        rPutStrLn (T.unpack (srInput line))+                        rPutStr (srLog line)++              rPutStrLn ""+              rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures)++              pure emptyCommandResult { crSuccess = failures == 0 }

@@ -8,8 +8,9 @@ import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Set as Set-import Data.Maybe(fromMaybe)+import Data.Maybe(fromMaybe, maybeToList) import Data.List(intersperse)+import Data.Foldable (for_) import Control.Monad(when,guard,unless,msum,mplus)  import Cryptol.Utils.PP@@ -26,7 +27,7 @@  import Cryptol.REPL.Monad -helpForNamed :: P.PName -> REPL ()+helpForNamed :: P.PName -> REPL Bool helpForNamed qname =   do fe <- getFocusedEnv      let params = M.mctxParams fe@@ -47,8 +48,11 @@          separ = rPutStrLn "            ---------"      sequence_ (intersperse separ helps) -     when (null (vNames ++ cNames ++ tNames ++ mNames)) $+     let failure = null (vNames ++ cNames ++ tNames ++ mNames)+     when failure $        rPrint $ "Undefined name:" <+> pp qname+    +     pure (not failure)   noInfo :: NameDisp -> M.Name -> REPL ()@@ -90,7 +94,7 @@                       , addV <$> fromD                       , addM <$> msum [ fromM, fromS, fromF ]                       ]-    where+    where      addT (k,d) = ns { msTypes = T.ModTParam { T.mtpName = x                                             , T.mtpKind = k                                             , T.mtpDoc  = d@@ -121,7 +125,7 @@                pure (M.AFunctor, M.ifsDoc (M.ifNames def))      fromS = do def <- Map.lookup x (M.ifSignatures env)-               pure (M.ASignature, T.mpnDoc def)+               pure (M.ASignature, maybeToList (T.mpnDoc def))   @@ -141,7 +145,7 @@ showSigHelp ::   M.IfaceDecls -> NameDisp -> M.Name -> T.ModParamNames -> REPL () showSigHelp _env _nameEnv name info =-  showSummary M.ASignature name (T.mpnDoc info)+  showSummary M.ASignature name (maybeToList (T.mpnDoc info))     emptySummary       { msTypes = Map.elems (T.mpnTypes info)       , msVals  = Map.elems (T.mpnFuns info)@@ -154,7 +158,7 @@   , msConstraints :: [T.Prop]   , msTypes       :: [T.ModTParam]   , msVals        :: [T.ModVParam]-  , msMods        :: [ (M.Name, M.ModKind, Maybe Text) ]+  , msMods        :: [ (M.Name, M.ModKind, [Text]) ]   }  emptySummary :: ModSummary@@ -166,7 +170,7 @@   , msMods        = []   } -showSummary :: M.ModKind -> M.Name -> Maybe Text -> ModSummary -> REPL ()+showSummary :: M.ModKind -> M.Name -> [Text] -> ModSummary -> REPL () showSummary k name doc info =   do rPutStrLn "" @@ -382,11 +386,10 @@     | otherwise       = "Provided by `parameters` declaration."  -doShowDocString :: Maybe Text -> REPL ()+doShowDocString :: Foldable f => f Text -> REPL () doShowDocString doc =-  case doc of-    Nothing -> pure ()-    Just d  -> rPutStrLn ('\n' : Text.unpack d)+  for_ doc $ \d ->+    rPutStrLn ('\n' : Text.unpack d)  ppFixity :: T.Fixity -> String ppFixity f = "Precedence " ++ show (P.fLevel f) ++ ", " ++

@@ -24,6 +24,7 @@   , raise   , stop   , catch+  , try   , finally   , rPutStrLn   , rPutStr@@ -48,7 +49,7 @@   , getTypeNames   , getPropertyNames   , getModNames-  , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod+  , LoadedModule(..), lName, getLoadedMod, setLoadedMod, clearLoadedMod   , setEditPath, getEditPath, clearEditPath   , setSearchPath, prependSearchPath   , getPrompt@@ -57,6 +58,7 @@   , asBatch   , validEvalContext   , updateREPLTitle+  , isolated   , setUpdateREPLTitle   , withRandomGen   , setRandomGen@@ -79,12 +81,17 @@     -- ** Configurable Output   , getPutStr   , getLogger+  , setLogger   , setPutStr      -- ** Smoke Test   , smokeTest   , Smoke(..) +  , RW(..)+  , defaultRW+  , mkUserEnv+   ) where  import Cryptol.REPL.Trie@@ -145,10 +152,13 @@  -- | This indicates what the user would like to work on. data LoadedModule = LoadedModule-  { lName :: Maybe P.ModName  -- ^ Working on this module.-  , lPath :: M.ModulePath     -- ^ Working on this file.+  { lFocus :: Maybe (P.ImpName T.Name) -- ^ Working on this module.+  , lPath :: M.ModulePath -- ^ Working on this file.   } +lName :: LoadedModule -> Maybe P.ModName+lName lm = M.impNameTopModule <$> lFocus lm+ -- | REPL RW Environment. data RW = RW   { eLoadedMod   :: Maybe LoadedModule@@ -232,14 +242,15 @@   detailedPrompt = id False    modLn   =-    case lName =<< eLoadedMod rw of+    case lFocus =<< eLoadedMod rw of       Nothing -> show (pp I.preludeName)       Just m         | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)"         | M.isLoadedInterface m loaded -> modName ++ "(interface)"         | otherwise -> modName-        where modName = pretty m-              loaded = M.meLoadedModules (eModuleEnv rw)+        where +          modName = pretty m+          loaded = M.meLoadedModules (eModuleEnv rw)    withFocus =     case eLoadedMod rw of@@ -392,6 +403,9 @@ catch :: REPL a -> (REPLException -> REPL a) -> REPL a catch m k = REPL (\ ref -> rethrowEvalError (unREPL m ref) `X.catch` \ e -> unREPL (k e) ref) +try :: REPL a -> REPL (Either REPLException a)+try m = REPL (X.try . rethrowEvalError . unREPL m)+ finally :: REPL a -> REPL b -> REPL a finally m1 m2 = REPL (\ref -> unREPL m1 ref `X.finally` unREPL m2 ref) @@ -499,7 +513,7 @@ clearLoadedMod :: REPL () clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw })                     updateREPLTitle-  where upd x = x { lName = Nothing }+  where upd x = x { lFocus = Nothing }  -- | Set the name of the currently focused file, loaded via @:r@. setLoadedMod :: LoadedModule -> REPL ()@@ -560,26 +574,17 @@   modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch })   return a --- | Is evaluation enabled.  If the currently focused module is--- parameterized, then we cannot evalute.+isolated :: REPL a -> REPL a+isolated body = do+  rw <- getRW+  body `finally` modifyRW_ (const rw)++-- | Is evaluation enabled? If the currently focused module is parameterized,+-- then we cannot evaluate. validEvalContext :: T.FreeVars a => a -> REPL () validEvalContext a =   do me <- eModuleEnv <$> getRW-     let ds      = T.freeVars a-         badVals = foldr badName Set.empty (T.valDeps ds)-         bad     = foldr badName badVals (T.tyDeps ds)-         badTs   = T.tyParams ds--         badName nm bs =-           case M.nameInfo nm of--             -- XXX: Changes if focusing on nested modules-             M.GlobalName _ I.OrigName { ogModule = I.TopModule m }-               | M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs-               | M.isLoadedInterface m (M.meLoadedModules me) -> Set.insert nm bs--             _ -> bs-+     let (badTs, bad) = M.loadedParamModDeps (M.meLoadedModules me) a      unless (Set.null bad && Set.null badTs) $        raise (EvalInParamModule (Set.toList badTs) (Set.toList bad)) @@ -606,6 +611,8 @@ getLogger :: REPL Logger getLogger = eLogger <$> getRW +setLogger :: Logger -> REPL ()+setLogger logger = modifyRW_ $ \rw -> rw { eLogger = logger }  -- | Use the configured output action to print a string rPutStr :: String -> REPL ()@@ -752,12 +759,13 @@   return (optName opt, optDefault opt)  -- | Set a user option.-setUser :: String -> String -> REPL ()+-- Returns 'True' on success+setUser :: String -> String -> REPL Bool setUser name val = case lookupTrieExact name userOptionsWithAliases of    [opt] -> setUserOpt opt-  []    -> rPutStrLn ("Unknown env value `" ++ name ++ "`")-  _     -> rPutStrLn ("Ambiguous env value `" ++ name ++ "`")+  []    -> False <$ rPutStrLn ("Unknown env value `" ++ name ++ "`")+  _     -> False <$ rPutStrLn ("Ambiguous env value `" ++ name ++ "`")    where   setUserOpt opt = case optDefault opt of@@ -766,25 +774,26 @@     EnvProg _ _ ->       case splitOptArgs val of         prog:args -> doCheck (EnvProg prog args)-        [] -> rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`")+        [] -> False <$ rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`")      EnvNum _ -> case reads val of       [(x,_)] -> doCheck (EnvNum x)-      _ -> rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`")+      _ -> False <$ rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`")      EnvBool _       | any (`isPrefixOf` val) ["enable", "on", "yes", "true"] ->-        writeEnv (EnvBool True)+        True <$ writeEnv (EnvBool True)       | any (`isPrefixOf` val) ["disable", "off", "no", "false"] ->-        writeEnv (EnvBool False)+        True <$ writeEnv (EnvBool False)       | otherwise ->-        rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`")+        False <$ rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`")     where     doCheck v = do (r,ws) <- optCheck opt v                    case r of-                     Just err -> rPutStrLn err+                     Just err -> False <$ rPutStrLn err                      Nothing  -> do mapM_ rPutStrLn ws                                     writeEnv v+                                    pure True     writeEnv ev =       do optEff opt ev          modifyRW_ (\rw -> rw { eUserEnv = Map.insert (optName opt) ev (eUserEnv rw) })@@ -1006,6 +1015,9 @@   , simpleOpt "proverStats" ["prover-stats"] (EnvBool True) noCheck     "Enable prover timing statistics." +  , simpleOpt "proverTimeout" ["prover-timeout"] (EnvNum 0) checkTimeout+    "Specify timeout in seconds for online prover processes."+   , simpleOpt "proverValidate" ["prover-validate"] (EnvBool False) noCheck     "Validate :sat examples and :prove counter-examples for correctness." @@ -1074,6 +1086,14 @@ parseFieldOrder "canonical" = Just CanonicalOrder parseFieldOrder "display" = Just DisplayOrder parseFieldOrder _ = Nothing++checkTimeout :: Checker+checkTimeout val =+  case val of+    EnvNum n+      | n < 0 -> noWarns (Just "timeout should be non-negative")+      | otherwise -> noWarns Nothing+    _ -> noWarns (Just "Failed to parse `prover-timeout`")  checkFieldOrder :: Checker checkFieldOrder val =

@@ -45,6 +45,7 @@ import qualified Data.SBV as SBV (sObserve, symbolicEnv) import qualified Data.SBV.Internals as SBV (SBV(..)) import qualified Data.SBV.Dynamic as SBV+import qualified Data.SBV.Trans.Control as SBV (SMTOption(..)) import           Data.SBV (Timing(SaveTiming))  import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)@@ -104,6 +105,17 @@   , ("sbv-any"      , SBV.defaultSMTCfg )   ] +setTimeoutSecs ::+  Int {- ^ seconds -} ->+  SBV.SMTConfig -> SBV.SMTConfig+setTimeoutSecs s cfg = cfg+  { SBV.solverSetOptions =+    SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] :+    filter (not . isTimeout) (SBV.solverSetOptions cfg) }+  where+    isTimeout (SBV.OptionKeyword k _) = k == ":timeout"+    isTimeout _ = False+ newtype SBVPortfolioException   = SBVPortfolioException [Either X.SomeException (Maybe String,String)] @@ -239,12 +251,13 @@ -- | Select the appropriate solver or solvers from the given prover command, --   and invoke those solvers on the given symbolic value. runProver ::+  Int ->   SBVProverConfig ->   ProverCommand ->   (String -> IO ()) ->   SBV.Symbolic SBV.SVal ->   IO (Maybe String, [SBV.SMTResult])-runProver proverConfig pc@ProverCommand{..} lPutStrLn x =+runProver timeoutSecs proverConfig pc@ProverCommand{..} lPutStrLn x =   do let mSatNum = case pcQueryType of                      SatQuery (SomeSat n) -> Just n                      SatQuery AllSat -> Nothing@@ -272,17 +285,20 @@                    | p <- ps])         SBVProverConfig p ->-         let p' = p { SBV.transcript = pcSmtFile+         let p1 = p { SBV.transcript = pcSmtFile                     , SBV.allSatMaxModelCount = mSatNum                     , SBV.timing = SaveTiming pcProverStats                     , SBV.verbose = pcVerbose                     , SBV.validateModel = pcValidate-                    } in+                    }+             p2 | timeoutSecs > 0 = setTimeoutSecs timeoutSecs p1+                | otherwise = p1+          in           case pcQueryType of-            ProveQuery  -> runSingleProver pc lPutStrLn p' SBV.proveWith thmSMTResults x-            SafetyQuery -> runSingleProver pc lPutStrLn p' SBV.proveWith thmSMTResults x-            SatQuery (SomeSat 1) -> runSingleProver pc lPutStrLn p' SBV.satWith satSMTResults x-            SatQuery _           -> runSingleProver pc lPutStrLn p' SBV.allSatWith allSatSMTResults x+            ProveQuery  -> runSingleProver pc lPutStrLn p2 SBV.proveWith thmSMTResults x+            SafetyQuery -> runSingleProver pc lPutStrLn p2 SBV.proveWith thmSMTResults x+            SatQuery (SomeSat 1) -> runSingleProver pc lPutStrLn p2 SBV.satWith satSMTResults x+            SatQuery _           -> runSingleProver pc lPutStrLn p2 SBV.allSatWith allSatSMTResults x   -- | Prepare a symbolic query by symbolically simulating the expression found in@@ -415,16 +431,16 @@        [] -> return $ ThmResult (unFinType <$> ts)         -- otherwise something is wrong-       _ -> return $ ProverError (rshow results)+       resultsHead:_ -> return $ ProverError res #if MIN_VERSION_sbv(10,0,0)-              where rshow | isSat = show . (SBV.AllSatResult False False False)+              where res | isSat = show $ SBV.AllSatResult False False False results                     -- sbv-10.0.0 removes the `allSatHasPrefixExistentials` field #elif MIN_VERSION_sbv(8,8,0)-              where rshow | isSat = show . (SBV.AllSatResult False False False False)+              where res | isSat = show $ SBV.AllSatResult False False False False results #else-              where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)+              where res | isSat = show $ SBV.AllSatResult (False,False,False,results) #endif-                          | otherwise = show . SBV.ThmResult . head+                        | otherwise = show $ SBV.ThmResult resultsHead    where   mkTevs prims result = do@@ -445,8 +461,8 @@ --   This command returns a pair: the first element is the name of the --   solver that completes the given query (if any) along with the result --   of executing the query.-satProve :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)-satProve proverCfg pc =+satProve :: SBVProverConfig -> Int -> ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)+satProve proverCfg timeoutSecs pc =   protectStack proverError $ \minp ->   M.runModuleM minp $ do   evo <- liftIO (M.minpEvalOpts minp)@@ -456,7 +472,7 @@   prepareQuery evo pc >>= \case     Left msg -> return (Nothing, ProverError msg)     Right (ts, q) ->-      do (firstProver, results) <- M.io (runProver proverCfg pc lPutStrLn q)+      do (firstProver, results) <- M.io (runProver timeoutSecs proverCfg pc lPutStrLn q)          esatexprs <- processResults pc ts results          return (firstProver, esatexprs) 

@@ -41,7 +41,7 @@ import System.IO (Handle, IOMode(..), withFile) import Data.Time import Data.IORef-import Data.List (intercalate, tails, inits)+import Data.List (intercalate, inits) import Data.List.NonEmpty (NonEmpty(..)) import Data.Proxy import qualified Data.Map as Map@@ -261,6 +261,7 @@     test =       do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator          W4.extendConfig opts (W4.getConfiguration sym)+          (proc :: W4.SolverProcess GlobalNonceGenerator s) <- W4.startSolverProcess fs Nothing sym          res <- W4.checkSatisfiable proc "smoke test" (W4.falsePred sym)          case res of@@ -380,10 +381,11 @@   W4ProverConfig ->   Bool {- ^ hash consing -} ->   Bool {- ^ warn on uninterpreted functions -} ->+  Int {- ^ timeout milliseconds -} ->   ProverCommand ->   M.ModuleCmd (Maybe String, ProverResult) -satProve solverCfg hashConsing warnUninterp pc@ProverCommand {..} =+satProve solverCfg hashConsing warnUninterp timeoutMs pc@ProverCommand {..} =   protectStack proverError \modIn ->   M.runModuleM modIn   do w4sym   <- liftIO makeSym@@ -409,6 +411,7 @@                                   globalNonceGenerator        setupAdapterOptions solverCfg w4sym        when hashConsing (W4.startCaching w4sym)+       when (timeoutMs > 0) (setTimeout (fromIntegral timeoutMs) w4sym)        pure w4sym    doLog lg () =@@ -470,7 +473,7 @@   makeSym =     do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator        W4.extendConfig W4.z3Options (W4.getConfiguration sym)-       when hashConsing  (W4.startCaching sym)+       when hashConsing (W4.startCaching sym)        pure sym    onError msg minp = pure (Right (Just msg, M.minpModuleEnv minp), [])@@ -631,7 +634,7 @@   | prefix <- inits (zip vs cs)   | v      <- vs   | c      <- cs-  | tl     <- tail (tails vs)+  | tl     <- NE.tail (NE.tails vs)   ] -- == END Support operations for multi-SAT == @@ -754,3 +757,18 @@     VarEnum tag cons ->       VarEnum <$> W4.groundEval evalFn tag               <*> traverse (traverse (varShapeToConcrete evalFn)) cons++symCfg :: (W4.IsExprBuilder sym, W4.Opt t a) => sym -> W4.ConfigOption t -> a -> IO ()+symCfg sym x y =+ do opt <- W4.getOptionSetting x (W4.getConfiguration sym)+    _   <- W4.trySetOpt opt y+    pure ()++setTimeout :: W4.IsExprBuilder sym => Integer -> sym -> IO ()+setTimeout s sym =+ do symCfg sym W4.z3Timeout (1000 * s)+    symCfg sym W4.cvc4Timeout (1000 * s)+    symCfg sym W4.cvc5Timeout (1000 * s)+    symCfg sym W4.boolectorTimeout (1000 * s)+    symCfg sym W4.yicesGoalTimeout s -- N.B. yices takes seconds+    pure ()

@@ -28,13 +28,12 @@   , Fixity(..)   , PrimMap(..)   , module Cryptol.TypeCheck.Type+  , DocFor(..)   ) where -import Data.Maybe(mapMaybe)- import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)-import Cryptol.Parser.Position(Located,Range,HasLoc(..))+import Cryptol.Parser.Position(Located, HasLoc(..), Range) import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.ModuleSystem.Interface@@ -55,11 +54,12 @@ import Control.DeepSeq  -import           Data.Set    (Set)+import qualified Data.IntMap as IntMap import           Data.Map    (Map) import qualified Data.Map    as Map-import qualified Data.IntMap as IntMap-import           Data.Text (Text)+import           Data.Maybe  (mapMaybe, maybeToList)+import           Data.Set    (Set)+import           Data.Text   (Text)   data TCTopEntity =@@ -84,7 +84,7 @@ -- | A Cryptol module. data ModuleG mname =               Module { mName             :: !mname-                     , mDoc              :: !(Maybe Text)+                     , mDoc              :: ![Text]                      , mExports          :: ExportSpec Name                       -- Functors:@@ -109,7 +109,7 @@                      , mTySyns           :: Map Name TySyn                      , mNominalTypes     :: Map Name NominalType                      , mDecls            :: [DeclGroup]-                     , mSubmodules       :: Map Name (IfaceNames Name)+                     , mSubmodules       :: Map Name Submodule                      , mSignatures       :: !(Map Name ModParamNames)                       , mInScope          :: NamingEnv@@ -117,11 +117,16 @@                        --   Submodule in-scope information is in 'mSubmodules'.                      } deriving (Show, Generic, NFData) +data Submodule = Submodule+  { smIface :: IfaceNames Name+  , smInScope :: NamingEnv+  } deriving (Show, Generic, NFData)+ emptyModule :: mname -> ModuleG mname emptyModule nm =   Module     { mName             = nm-    , mDoc              = Nothing+    , mDoc              = mempty     , mExports          = mempty      , mParams           = mempty@@ -363,7 +368,7 @@                          , hang "where" 2 (vcat (map ppW ds))                          ] -      EPropGuards guards _ -> +      EPropGuards guards _ ->         parens (text "propguards" <+> vsep (ppGuard <$> guards))         where ppGuard (props, e) = indent 1                                  $ pipe <+> commaSep (ppW <$> props)@@ -522,3 +527,65 @@      TCTopModule m -> ppWithNames nm m      TCTopSignature n ps ->         hang ("interface module" <+> pp n <+> "where") 2 (pp ps)++data DocItem = DocItem+  { docModContext :: ImpName Name -- ^ The module scope to run repl commands in+  , docFor        :: DocFor -- ^ The name the documentation is attached to+  , docText       :: [Text] -- ^ The text of the attached docstring, if any+  }++data DocFor+  = DocForMod (ImpName Name)+  | DocForDef Name -- definitions that aren't modules++instance PP DocFor where+  ppPrec p x =+    case x of+      DocForMod m -> ppPrec p m+      DocForDef n -> ppPrec p n +++gatherModuleDocstrings ::+  Map Name (ImpName Name) ->+  Module ->+  [DocItem]+gatherModuleDocstrings nameToModule m =+  [DocItem+    { docModContext = ImpTop (mName m)+    , docFor = DocForMod (ImpTop (mName m))+    , docText = mDoc m+    }+  ] +++  -- mParams m+  -- mParamTypes m+  -- mParamFuns m+  [DocItem+    { docModContext = lookupModuleName n+    , docFor = DocForDef n+    , docText = maybeToList (tsDoc t)+    } | (n, t) <- Map.assocs (mTySyns m)] +++  [DocItem+    { docModContext = lookupModuleName n+    , docFor = DocForDef n+    , docText = maybeToList (ntDoc t)+    } | (n, t) <- Map.assocs (mNominalTypes m)] +++  [DocItem+    { docModContext = lookupModuleName (dName d)+    , docFor = DocForDef (dName d)+    , docText = maybeToList (dDoc d)+    } | g <- mDecls m, d <- groupDecls g] +++  [DocItem+    { docModContext = ImpNested n+    , docFor = DocForMod (ImpNested n)+    , docText = ifsDoc (smIface s)+    } | (n, s) <- Map.assocs (mSubmodules m)] +++  [DocItem+    { docModContext = ImpTop (mName m)+    , docFor = DocForMod (ImpNested n)+    , docText = maybeToList (mpnDoc s)+    } | (n, s) <- Map.assocs (mSignatures m)]+  where+    lookupModuleName n =+      case Map.lookup n nameToModule of+        Just x -> x+        Nothing -> panic "gatherModuleDocstrings" ["No owning module for name:", show (pp n)]

@@ -6,10 +6,11 @@ module Cryptol.TypeCheck.Error where  import qualified Data.IntMap as IntMap+import qualified Data.List.NonEmpty as NE import qualified Data.Set as Set import Control.DeepSeq(NFData) import GHC.Generics(Generic)-import Data.List((\\),sortBy,groupBy,partition)+import Data.List((\\),sortBy,partition) import Data.Function(on)  import Cryptol.Utils.Ident(Ident,Namespace(..))@@ -32,14 +33,15 @@    -- pick shortest error from each location.   dropErrorsFromSameLoc = concatMap chooseBestError-                        . groupBy ((==)    `on` fst)+                        . NE.groupBy ((==)    `on` fst)    addErrorRating (r,e) = (errorImportance e, (r,e))-  chooseBestError    = map snd-                     . head-                     . groupBy ((==) `on` fst)-                     . sortBy (flip compare `on` fst)-                     . map addErrorRating+  chooseBestError    = NE.toList+                     . fmap snd+                     . NE.head+                     . NE.groupBy1 ((==) `on` fst)+                     . NE.sortBy (flip compare `on` fst)+                     . fmap addErrorRating     cmpR r  = ( source r    -- First by file@@ -169,13 +171,6 @@               | UnsupportedFFIType TypeSource FFITypeError                 -- ^ Type is not supported for FFI -              | NestedConstraintGuard Ident-                -- ^ Constraint guards may only apper at the top-level--              | DeclarationRequiresSignatureCtrGrd Ident-                -- ^ All declarataions in a recursive group involving-                -- constraint guards should have signatures-               | InvalidConstraintGuard Prop                 -- ^ The given constraint may not be used as a constraint guard @@ -271,8 +266,6 @@     UnsupportedFFIType {}                            -> 7     -- less than UnexpectedTypeWildCard -    NestedConstraintGuard {}                         -> 10-    DeclarationRequiresSignatureCtrGrd {}            -> 9     InvalidConstraintGuard {}                        -> 5  @@ -340,8 +333,6 @@       UnsupportedFFIKind {}    -> err       UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e -      NestedConstraintGuard {} -> err-      DeclarationRequiresSignatureCtrGrd {} -> err       InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p        TemporaryError {} -> err@@ -393,8 +384,6 @@       UnsupportedFFIKind {}  -> Set.empty       UnsupportedFFIType _ t -> fvs t -      NestedConstraintGuard {} -> Set.empty-      DeclarationRequiresSignatureCtrGrd {} -> Set.empty       InvalidConstraintGuard p -> fvs p        TemporaryError {} -> Set.empty@@ -685,18 +674,6 @@       UnsupportedFFIType src t -> vcat         [ ppWithNames names t         , "When checking" <+> pp src ]--      NestedConstraintGuard d ->-        vcat [ "Local declaration" <+> backticks (pp d)-                                   <+> "may not use constraint guards."-             , "Constraint guards may only appear at the top-level of a module."-             ]--      DeclarationRequiresSignatureCtrGrd d ->-        vcat [ "The declaration of" <+> backticks (pp d) <+>-                                            "requires a full type signature,"-             , "because it is part of a recursive group with constraint guards."-             ]        InvalidConstraintGuard p ->         let d = case tNoUser p of

@@ -63,7 +63,7 @@ import qualified Data.Set as Set import           Data.List(foldl', sortBy, groupBy, partition) import           Data.Either(partitionEithers)-import           Data.Maybe(isJust, fromMaybe, mapMaybe)+import           Data.Maybe(isJust, fromMaybe, mapMaybe, maybeToList) import           Data.Ratio(numerator,denominator) import           Data.Traversable(forM) import           Data.Function(on)@@ -77,14 +77,14 @@ inferTopModule m =   case P.mDef m of     P.NormalModule ds ->-      do newModuleScope (thing (P.mName m)) (P.exportedDecls ds) (P.mInScope m)+      do newModuleScope (maybeToList (thing <$> P.mDocTop m)) (thing (P.mName m)) (P.exportedDecls ds) (P.mInScope m)          checkTopDecls ds          proveModuleTopLevel          endModule      P.FunctorInstance f as inst ->       do mb <- doFunctorInst-           (P.ImpTop <$> P.mName m) f as inst (P.mInScope m) Nothing+           (P.ImpTop <$> P.mName m) f as inst (P.mInScope m) (thing <$> P.mDocTop m)          case mb of            Just mo -> pure mo            Nothing -> panic "inferModule" ["Didnt' get a module"]@@ -739,11 +739,8 @@ -- an enum, throwing an error if this is not the case. expectEnum :: Type -> InferM [EnumCon] expectEnum ty =-  case ty of-    TUser _ _ ty' ->-      expectEnum ty'--    TNominal nt _+  case tIsNominal ty of+    Just (nt, _)       |  Enum ecs <- ntDef nt       -> pure ecs @@ -956,8 +953,6 @@                      genCs     <- generalize bs1 cs                      return (done,genCs) -     checkNumericConstraintGuardsOK isTopLevel sigs noSigs-      rec        let exprMap = Map.fromList (map monoUse genBs)        (doneBs, genBs) <- check exprMap@@ -985,40 +980,6 @@     withQs   = foldl' appP withTys  qs  -{--Here we also check that:-  * Numeric constraint guards appear only at the top level-  * All definitions in a recursive groups with numberic constraint guards-    have signatures--The reason is to avoid interference between local constraints coming-from the guards and type inference.  It might be possible to-relex these requirements, but this requires some more careful thought on-the interaction between the two, and the effects on pricniple types.--}-checkNumericConstraintGuardsOK ::-  Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()-checkNumericConstraintGuardsOK isTopLevel haveSig noSig =-  do unless isTopLevel-            (mapM_ (mkErr NestedConstraintGuard) withGuards)-     unless (null withGuards)-            (mapM_ (mkErr DeclarationRequiresSignatureCtrGrd) noSig)-  where-  mkErr f b =-    do let nm = P.bName b-       inRange (srcRange nm) (recordError (f (nameIdent (thing nm))))--  withGuards = filter hasConstraintGuards haveSig-  -- When desugaring constraint guards we check that they have signatures,-  -- so no need to look at noSig--  hasConstraintGuards b =-    case P.bindImpl b of-      Just (P.DPropGuards {}) -> True-      _                       -> False--- {- | Come up with a type for recursive calls to a function, and decide      how we are going to be checking the binding.      Returns: (Name, type or schema, computation to check binding)@@ -1175,9 +1136,12 @@                          , dPragmas = P.bPragmas b                          , dInfix = P.bInfix b                          , dFixity = P.bFixity b-                         , dDoc = P.bDoc b+                         , dDoc = thing <$> P.bDoc b                          } +        -- The pass in Cryptol.Parser.ExpandPropGuards ensures that by the time+        -- we reach this code, all definitions that use constraint guards will+        -- have a type signature, so this case should be unreachable.         P.DPropGuards _ ->           tcPanic "checkMonoB"             [ "Used constraint guards without a signature at "@@ -1197,7 +1161,7 @@         , dPragmas    = P.bPragmas b         , dInfix      = P.bInfix b         , dFixity     = P.bFixity b-        , dDoc        = P.bDoc b+        , dDoc        = thing <$> P.bDoc b         }      P.DForeign mi -> do@@ -1231,7 +1195,7 @@                     , dPragmas    = P.bPragmas b                     , dInfix      = P.bInfix b                     , dFixity     = P.bFixity b-                    , dDoc        = P.bDoc b+                    , dDoc        = thing <$> P.bDoc b                     }      P.DImpl i -> do@@ -1243,7 +1207,7 @@         , dPragmas    = P.bPragmas b         , dInfix      = P.bInfix b         , dFixity     = P.bFixity b-        , dDoc        = P.bDoc b+        , dDoc        = thing <$> P.bDoc b         }    where@@ -1266,7 +1230,12 @@         P.DPropGuards cases0 -> do           asmps1 <- applySubstPreds asmps0           t1     <- applySubst t0-          cases1 <- mapM checkPropGuardCase cases0+          cases1 <- mapM (checkPropGuardCase asmps1) cases0+          -- If we recorded any errors when type-checking the constraint guards,+          -- then abort early. We don't want to check exhaustivity if there are+          -- malformed constraints, as these can cause panics elsewhere during+          -- exhaustivity checking (see the `issue{1593,1693}` test cases).+          abortIfErrors            exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)           unless exh $@@ -1395,19 +1364,62 @@   canProve asmps' goals =     tryProveImplication (Just (thing name)) as asmps' goals -{- | This function does not validate anything---it just translates into-the type-checkd syntax.  The actual validation of the guard will happen-when the (automatically generated) function corresponding to the guard is-checked, assuming 'ExpandpropGuards' did its job correctly.+{- | Generate type-checked syntax for the code in a PropGuard. For example,+consider the following (pre–type-checked) syntax for a guard: +@+f : {n, a} (Zero a) => [n]a+f | n == 1 => f(n == 1)+  | ...++f(n == 2) : {n, a} (Zero a, n == 1) => [n] a+f(n == 2) = ...+@++This function will type-check the `n == 1` constraint in the guard as well+as the f(n == 1) application on the right-hand side of the guard. This function+is responsible for ensuring that f(n == 1) is applied to the appropriate number+of type and proof arguments, so the type-checked syntax will look something+like:++@+f : {n, a} (Zero a) => [n]a+f | n == 1 => f(n == 1)`{n, a} <Zero a> <n == 1>+  | ...+@++Note that 'checkPropGuardCase' does not validate anything about the+(automatically generated) functions corresponding to guards (e.g., f(n == 1)).+These guard functions will be validated when the bodies of these functions are+type-checked, assuming "Cryptol.Parser.ExpandPropGuards" did its job correctly. -}-checkPropGuardCase :: P.PropGuardCase Name -> InferM ([Prop],Expr)-checkPropGuardCase (P.PropGuardCase guards e0) =-  do ps <- checkPropGuards guards+checkPropGuardCase ::+  [Prop]+    {- ^ The constraints from the type signature. -} ->+  P.PropGuardCase Name+    {- ^ The guard itself. -} ->+  InferM ([Prop],Expr)+    {- ^ The type-checked guard constraints and right-hand side expression. -}+checkPropGuardCase asmps (P.PropGuardCase guards e0) =+  do -- First, validate the constraints in the guard.+     ps <- checkPropGuards guards+     -- Next, take the application of the guard function on the right-hand side+     -- and decompose it into the name of the function `eV`, the type arguments+     -- `ts`, and the value arguments `es`.+     --+     -- To do this, we kind-check all of the type arguments...      tys <- mapM (`checkType` Nothing) ts-     let rhsTs = foldl ETApp                  (getV eV) tys-         rhsPs = foldl (\e _p -> EProofApp e) rhsTs     ps-         rhs   = foldl EApp                   rhsPs     (map getV es)+     let -- ...then apply the guard function to the kind-checked types...+         rhsTs = foldl ETApp (getV eV) tys+         -- ...then apply that to the constraints from the type signature+         -- (`asmps`) and the constraints in the guard (`ps`). Note that `asmps`+         -- is guaranteed to contain all of the non-guard constraints in scope,+         -- as numeric constraint guards can only be used in top-level (i.e.,+         -- non-local) functions...+         rhsPs = foldl (\e _p -> EProofApp e) rhsTs (asmps ++ ps)+         -- ...finally, apply that to the value arguments. If `ExpandPropGuards`+         -- did its job correctly, all value arguments should be variables.+         rhs = foldl EApp rhsPs (map getV es)      pure (ps,rhs)    where@@ -1424,7 +1436,7 @@   getT ti =     case ti of       P.PosInst t    -> t-      P.NamedInst {} -> bad "Unexpeceted NamedInst"+      P.NamedInst {} -> bad "Unexpected NamedInst"    bad msg = panic "checkPropGuardCase" [msg] @@ -1472,7 +1484,7 @@             P.NormalModule ds ->              do newSubmoduleScope (thing (P.mName m))-                                  (thing <$> P.tlDoc tl)+                                  (maybeToList (thing <$> P.tlDoc tl))                                   (P.exportedDecls ds)                                   (P.mInScope m)                 checkTopDecls ds@@ -1486,7 +1498,7 @@                 pure ()             P.InterfaceModule sig ->-              do let doc = P.thing <$> P.tlDoc tl+              do let doc = thing <$> P.tlDoc tl                  inRange (srcRange (P.mName m))                    do newSignatureScope (thing (P.mName m)) doc                       checkSignature sig@@ -1612,7 +1624,7 @@      let n = thing (P.pfName x)      return ModVParam { mvpName = n                       , mvpType = s-                      , mvpDoc  = P.pfDoc x+                      , mvpDoc  = thing <$> P.pfDoc x                       , mvpFixity = P.pfFixity x                       } 

@@ -51,7 +51,8 @@   where   nestedInSet = Set.unions . map inNested . Set.toList   inNested x  = case Map.lookup x (mSubmodules m) of-                  Just y  -> ifsDefines y `Set.union` nestedInSet (ifsNested y)+                  Just y  -> ifsDefines iface `Set.union` nestedInSet (ifsNested iface)+                    where iface = smIface y                   Nothing -> Set.empty -- must be signature or a functor  genIface :: ModuleG name -> IfaceG name@@ -71,7 +72,7 @@                                        , d  <- groupDecls dg                                        , let qn = dName d                                        ]-    , ifModules         = mSubmodules m+    , ifModules         = smIface <$> mSubmodules m     , ifSignatures      = mSignatures m     , ifFunctors        = genIface <$> mFunctors m     }

@@ -98,7 +98,7 @@   do let mbDoc = P.ptDoc a          k = cvtK (P.ptKind a)          n = thing (P.ptName a)-     return ModTParam { mtpKind = k, mtpName = n, mtpDoc = mbDoc }+     return ModTParam { mtpKind = k, mtpName = n, mtpDoc = thing <$> mbDoc }   -- | Check a type-synonym declaration.

@@ -4,6 +4,7 @@ import Data.List(partition,unzip4) import Data.Text(Text) import Data.Map(Map)+import Data.Maybe (maybeToList) import qualified Data.Map as Map import qualified Data.Map.Merge.Strict as Map import Data.Set (Set)@@ -42,7 +43,7 @@   -} ->   NamingEnv   {- ^ Names in the enclosing scope of the instantiated module -} ->-  Maybe Text                  {- ^ Documentation -} ->+  Maybe Text                  {- ^ Documentation for the module being generated -} ->   InferM (Maybe TCTopEntity) doFunctorInst m f as instMap0 enclosingInScope doc =   inRange (srcRange m)@@ -57,7 +58,7 @@                   ?nameSu = instMap <> mconcat paramInstMaps               let m1   = moduleInstance mf                   m2   = m1 { mName             = m-                            , mDoc              = Nothing+                            , mDoc              = mempty                             , mParamTypes       = mempty                             , mParamFuns        = mempty                             , mParamConstraints = mempty@@ -98,14 +99,20 @@            mconcat [ modParamNamingEnv mp | (_, mp, AddDeclParams) <- argIs ]          inScope = inScope0 `shadowing` enclosingInScope +     -- Combine the docstrings of:+     -- * The functor being instantiated+     -- * The module being generated+     let newDoc = maybeToList doc <> mDoc mf+      case thing m of-       P.ImpTop mn    -> newModuleScope mn (mExports m2) inScope-       P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) inScope+       P.ImpTop mn    -> newModuleScope newDoc mn (mExports m2) inScope+       P.ImpNested mn -> newSubmoduleScope mn newDoc (mExports m2) inScope       mapM_ addTySyn     (Map.elems (mTySyns m2))      mapM_ addNominal   (Map.elems (mNominalTypes m2))      addSignatures      (mSignatures m2)      addSubmodules      (mSubmodules m2)+     setNested          (mNested m2)      addFunctors        (mFunctors m2)      mapM_ addDecls     (mDecls m2) @@ -137,8 +144,11 @@   case args of      P.DefaultInstArg arg ->-      let i = Located { srcRange = srcRange arg-                      , thing    = head (Map.keys ps0)+      let p0 = case Map.keys ps0 of+                 p':_ -> p'+                 [] -> panic "checkArity" ["functor with no parameters"]+          i = Located { srcRange = srcRange arg+                      , thing    = p0                       }       in checkArgs [] ps0 [ P.ModuleInstanceNamedArg i arg ] 

@@ -63,10 +63,16 @@       ImpTop t -> ImpTop t       ImpNested n -> ImpNested (moduleInstance n) +instance ModuleInstance Submodule where+  moduleInstance x = Submodule+    { smInScope = moduleInstance (smInScope x)+    , smIface = moduleInstance (smIface x)+    }+ instance ModuleInstance (ModuleG name) where   moduleInstance m =     Module { mName             = mName m-           , mDoc              = Nothing+           , mDoc              = mempty            , mExports          = doNameInst (mExports m)            , mParamTypes       = doMap (mParamTypes m)            , mParamFuns        = doMap (mParamFuns m)

@@ -772,7 +772,7 @@               Just a -> pure (ExtVar a)               Nothing ->                 do mp <- IM $ asks iVars-                   panic "lookupVar" $ [ "Undefined vairable"+                   panic "lookupVar" $ [ "Undefined variable"                                      , show x                                      , "IVARS"                                      ] ++ map (show . debugShowUniques . pp) (Map.keys mp)@@ -852,7 +852,7 @@       do localMods <- getScope mSubmodules          case Map.lookup m localMods of            Just names ->-              do n <- genIfaceWithNames names <$> getCurDecls+              do n <- genIfaceWithNames (smIface names) <$> getCurDecls                  pure (If.ifaceForgetName n)             Nothing ->@@ -998,16 +998,16 @@ to initialize an empty module.  As we type check declarations they are added to this module's scope. -} newSubmoduleScope ::-  Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> InferM ()+  Name -> [Text] -> ExportSpec Name -> NamingEnv -> InferM () newSubmoduleScope x docs e inScope =   do updScope \o -> o { mNested = Set.insert x (mNested o) }      newScope (SubModule x)      updScope \m -> m { mDoc = docs, mExports = e, mInScope = inScope } -newModuleScope :: P.ModName -> ExportSpec Name -> NamingEnv -> InferM ()-newModuleScope x e inScope =+newModuleScope :: [Text] -> P.ModName -> ExportSpec Name -> NamingEnv -> InferM ()+newModuleScope docs x e inScope =   do newScope (MTopModule x)-     updScope \m -> m { mDoc = Nothing, mExports = e, mInScope = inScope }+     updScope \m -> m { mDoc = docs, mExports = e, mInScope = inScope }  -- | Update the current scope (first in the list). Assumes there is one. updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()@@ -1057,7 +1057,10 @@                  , mSignatures  = add mSignatures                  , mSubmodules  = if isFun                                     then mSubmodules y-                                    else Map.insert m (genIfaceNames x1)+                                    else let sm = Submodule+                                                    { smIface = genIfaceNames x1+                                                    , smInScope = mInScope x }+                                         in Map.insert m sm                                                (mSubmodules x <> mSubmodules y)                  , mFunctors    = if isFun                                     then Map.insert m x1 (mFunctors y)@@ -1132,7 +1135,7 @@   mergeDecls m1 m2 =     Module       { mName             = ()-      , mDoc              = Nothing+      , mDoc              = mempty       , mExports          = mempty       , mParams           = mempty       , mParamTypes       = mempty@@ -1183,7 +1186,7 @@ addSignatures mp =   updScope \r -> r { mSignatures = Map.union mp (mSignatures r) } -addSubmodules :: Map Name (If.IfaceNames Name) -> InferM ()+addSubmodules :: Map Name Submodule -> InferM () addSubmodules mp =   updScope \r -> r { mSubmodules = Map.union mp (mSubmodules r) } @@ -1191,7 +1194,9 @@ addFunctors mp =   updScope \r -> r { mFunctors = Map.union mp (mFunctors r) } -+setNested :: Set Name -> InferM ()+setNested names =+  updScope \r -> r { mNested = names }   -- | The sub-computation is performed with the given abstract function in scope.

@@ -364,8 +364,12 @@       in go dgs  -    EPropGuards _guards typ -> -      pure Forall {sVars = [], sProps = [], sType = typ}+    EPropGuards guards typ ->+      do forM_ guards $ \(prop, e) ->+           do mapM_ (checkTypeIs KProp) prop+              eTyp <- exprType e+              sameTypes "EPropGuards" typ eTyp+         pure (tMono typ)   checkCaseAlt :: CaseAlt -> TcM ([Type], Type)

@@ -142,7 +142,8 @@   | Just n <- tIsNum x  = mulK n y   | Just n <- tIsNum y  = mulK n x   | Just v <- matchMaybe swapVars = v-  | otherwise           = tf2 TCMul x y+  | otherwise = checkExpMul x y+     where   mulK 0 _ = tNum (0 :: Int)   mulK 1 t = t@@ -154,8 +155,11 @@            , Just b' <- tIsNum b            -- XXX: similar for a = b * k?            , n == b' = tSub a (tMod a b)--+           -- c * c ^ x = c ^ (1 + x)+           | TCon (TF TCExp) [a,b] <- t'+           , Just n' <- tIsNum a+           , n == n' = tf2 TCExp a (tAdd (tNum (1::Int)) b)+           -- c^x * c^y = c ^ (y + x)            | otherwise = tf2 TCMul (tNum n) t     where t' = tNoUser t @@ -163,6 +167,14 @@                 b <- aTVar y                 guard (b < a)                 return (tf2 TCMul y x)+  +  -- Check if (K^a * K^b) => K^(a + b) otherwise default to standard mul+  checkExpMul s t | TCon (TF TCExp) [a,aExp] <- s+                  , Just a' <- tIsNum a+                  , TCon (TF TCExp) [b,bExp] <- t+                  , Just b' <- tIsNum b+                  , (a' >= 2 && a' == b') = tf2 TCExp a (tAdd aExp bExp)+                  | otherwise = tf2 TCMul x y   

@@ -48,6 +48,7 @@     <|> tryCancelVar ctxt (=#=) t1 t2     <|> tryLinearSolution t1 t2     <|> tryLinearSolution t2 t1+    <|> tryEqExp t1 t2  -- | Try to solve @t1 /= t2@ cryIsNotEqual :: Ctxt -> Type -> Type -> Solved@@ -67,6 +68,7 @@     <|> tryAddConst (>==) t1 t2     <|> tryCancelVar i (>==) t1 t2     <|> tryMinIsGeq t1 t2+    <|> tryGeqExp i t1 t2     -- XXX: k >= width e     -- XXX: width e >= k @@ -137,6 +139,17 @@   -- XXX: K1 ^^ n >= K2  +-- (K >= 2 && K^a >= K^b) => a >= b+tryGeqExp :: Ctxt -> Type -> Type -> Match Solved+tryGeqExp _ x y = +      do  (k_1, a) <- (|^|) x+          n <- aNat k_1+          guard (n >= 2)+          (k_2, b) <- (|^|) y+          guard (k_1 == k_2)+          return $ SolvedIf [ a >== b ]++ tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved tryGeqThanSub _ x y = @@ -223,6 +236,19 @@   +-- if (K >= 2) && K^a = K^b => a = b+tryEqExp :: Type -> Type -> Match Solved+tryEqExp x y = check x y <|> check y x+  where +    check i j =+      do  +          (k_1, a) <- (|^|) i+          n <- aNat k_1+          guard (n >= 2)+          (k_2, b) <- (|^|) j+          guard (k_1 == k_2)+          return $ SolvedIf [ a =#= b ]+   -- min t1 t2 = t1 ~> t1 <= t2 tryEqMin :: Type -> Type -> Match Solved tryEqMin x y =

@@ -33,6 +33,7 @@      -- * Lower level interactions   , inNewFrame, TVars, declareVars, assume, unsolvable+  , push, pop   ) where  import           SimpleSMT (SExpr)

@@ -599,6 +599,14 @@               TRec fs -> Just fs               _       -> Nothing +-- | If the supplied 'Type' is a 'TNominal' type, then return @'Just' (nt, ts)@,+-- where @nt@ and @ts@ are the underlying 'NominalType' and 'Type' arguments.+-- Otherwise, return 'Nothing'.+tIsNominal :: Type -> Maybe (NominalType, [Type])+tIsNominal ty = case tNoUser ty of+                  TNominal nm ts -> Just (nm, ts)+                  _              -> Nothing+ tIsBinFun :: TFun -> Type -> Maybe (Type,Type) tIsBinFun f ty = case tNoUser ty of                    TCon (TF g) [a,b] | f == g -> Just (a,b)@@ -965,7 +973,7 @@    where   bad = panic "pNegNumeric"-          [ "Unexpeceted numeric constraint:"+          [ "Unexpected numeric constraint:"           , pretty prop           ] 

@@ -56,6 +56,7 @@   , modParamIdent   , identAnonArg   , identAnonIfaceMod+  , identAnontInstImport   , identIsNormal      -- * Namespaces@@ -100,7 +101,7 @@ allNamespaces :: [Namespace] allNamespaces = [ minBound .. maxBound ] --- | Idnetifies a possibly nested module+-- | Identifies a possibly nested module data ModPath  = TopModule ModName               | Nested ModPath Ident                 deriving (Eq,Ord,Show,Generic,NFData)@@ -169,18 +170,17 @@ modNameArg :: ModName -> ModName modNameArg (ModName m fl) =   case fl of-    NormalName        -> ModName m AnonModArgName-    AnonModArgName    -> panic "modNameArg" ["Name is not normal"]-    AnonIfaceModName  -> panic "modNameArg" ["Name is not normal"]+    NormalName  -> ModName m AnonModArgName+    _           -> panic "modNameArg" ["Name is not normal"] + -- | Change a normal module name to a module name to be used for an -- anonnymous interface. modNameIfaceMod :: ModName -> ModName modNameIfaceMod (ModName m fl) =   case fl of     NormalName        -> ModName m AnonIfaceModName-    AnonModArgName    -> panic "modNameIfaceMod" ["Name is not normal"]-    AnonIfaceModName  -> panic "modNameIfaceMod" ["Name is not normal"]+    _                 -> panic "modNameIfaceMod" ["Name is not normal"]  -- | This is used when we check that the name of a module matches the -- file where it is defined.@@ -351,6 +351,10 @@ identAnonIfaceMod :: Ident -> Ident identAnonIfaceMod (Ident b _ txt) = Ident b AnonIfaceModName txt +-- | Make an anonymous identifier for an instantiation in an import.+identAnontInstImport :: Ident -> Ident+identAnontInstImport (Ident b _ txt) = Ident b AnonInstImport txt+ identIsNormal :: Ident -> Bool identIsNormal (Ident _ mb _) = isNormal mb @@ -360,6 +364,7 @@ data MaybeAnon = NormalName       -- ^ Not an anonymous name.                | AnonModArgName   -- ^ Anonymous module (from `where`)                | AnonIfaceModName -- ^ Anonymous interface (from `parameter`)+               | AnonInstImport   -- ^ Anonymous instance import   deriving (Eq,Ord,Show,Generic)  instance NFData MaybeAnon@@ -371,6 +376,7 @@     NormalName       -> txt     AnonModArgName   -> "`where` argument of " <> txt     AnonIfaceModName -> "`parameter` interface of " <> txt+    AnonInstImport   -> txt  isNormal :: MaybeAnon -> Bool isNormal mb =

@@ -430,4 +430,4 @@       NSModule    -> "/*module*/"  instance PP PrimIdent where-  ppPrec _ (PrimIdent m t) = pp m <.> text (T.unpack t)+  ppPrec _ (PrimIdent m t) = pp m <.> "::" <.> text (T.unpack t)