diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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 diff --git a/bench/Main.hs b/bench/Main.hs --- a/bench/Main.hs +++ b/bench/Main.hs @@ -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 diff --git a/cryptol.cabal b/cryptol.cabal --- a/cryptol.cabal +++ b/cryptol.cabal @@ -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 . 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 diff --git a/cryptol/Main.hs b/cryptol/Main.hs --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -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." diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs --- a/cryptol/REPL/Haskeline.hs +++ b/cryptol/REPL/Haskeline.hs @@ -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) diff --git a/cryptol/REPL/Logo.hs b/cryptol/REPL/Logo.hs --- a/cryptol/REPL/Logo.hs +++ b/cryptol/REPL/Logo.hs @@ -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 = diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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 ------------------------------------------- diff --git a/src/Cryptol/Backend/Arch.hs b/src/Cryptol/Backend/Arch.hs --- a/src/Cryptol/Backend/Arch.hs +++ b/src/Cryptol/Backend/Arch.hs @@ -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 diff --git a/src/Cryptol/Backend/FFI/Error.hs b/src/Cryptol/Backend/FFI/Error.hs --- a/src/Cryptol/Backend/FFI/Error.hs +++ b/src/Cryptol/Backend/FFI/Error.hs @@ -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)) <+> diff --git a/src/Cryptol/Eval/FFI/GenHeader.hs b/src/Cryptol/Eval/FFI/GenHeader.hs --- a/src/Cryptol/Eval/FFI/GenHeader.hs +++ b/src/Cryptol/Eval/FFI/GenHeader.hs @@ -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 diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -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 diff --git a/src/Cryptol/IR/FreeVars.hs b/src/Cryptol/IR/FreeVars.hs --- a/src/Cryptol/IR/FreeVars.hs +++ b/src/Cryptol/IR/FreeVars.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -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 } } diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -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 = diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -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) + ] diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -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) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -276,7 +276,6 @@ nameTopModule :: Name -> ModName nameTopModule = topModuleFor . nameModPath - -- Name Supply ----------------------------------------------------------------- class Monad m => FreshM m where diff --git a/src/Cryptol/ModuleSystem/Names.hs b/src/Cryptol/ModuleSystem/Names.hs --- a/src/Cryptol/ModuleSystem/Names.hs +++ b/src/Cryptol/ModuleSystem/Names.hs @@ -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 = diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs --- a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs +++ b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs @@ -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 } } - diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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 diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -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) } diff --git a/src/Cryptol/Parser/ExpandPropGuards.hs b/src/Cryptol/Parser/ExpandPropGuards.hs --- a/src/Cryptol/Parser/ExpandPropGuards.hs +++ b/src/Cryptol/Parser/ExpandPropGuards.hs @@ -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) diff --git a/src/Cryptol/Parser/Layout.hs b/src/Cryptol/Parser/Layout.hs --- a/src/Cryptol/Parser/Layout.hs +++ b/src/Cryptol/Parser/Layout.hs @@ -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, diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -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 diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -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? diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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 diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs --- a/src/Cryptol/Parser/Unlit.hs +++ b/src/Cryptol/Parser/Unlit.hs @@ -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 diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs --- a/src/Cryptol/Prelude.hs +++ b/src/Cryptol/Prelude.hs @@ -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") diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -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 diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -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 } diff --git a/src/Cryptol/REPL/Help.hs b/src/Cryptol/REPL/Help.hs --- a/src/Cryptol/REPL/Help.hs +++ b/src/Cryptol/REPL/Help.hs @@ -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) ++ ", " ++ diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -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 = diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs --- a/src/Cryptol/Symbolic/SBV.hs +++ b/src/Cryptol/Symbolic/SBV.hs @@ -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) diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -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 () diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -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)] diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -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} + | ... +@ + +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 } diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -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 } diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -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. diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -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 ] diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -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) diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -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. diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -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) diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs --- a/src/Cryptol/TypeCheck/SimpType.hs +++ b/src/Cryptol/TypeCheck/SimpType.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs --- a/src/Cryptol/TypeCheck/Solver/Numeric.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs @@ -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 = diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs --- a/src/Cryptol/TypeCheck/Solver/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/SMT.hs @@ -33,6 +33,7 @@ -- * Lower level interactions , inNewFrame, TVars, declareVars, assume, unsolvable + , push, pop ) where import SimpleSMT (SExpr) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -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 ] diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -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 = diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -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)