cryptol 3.4.0 → 3.5.0
raw patch · 47 files changed
+1236/−543 lines, 47 filesdep ~basePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base
API changes (from Hackage documentation)
Files
- CHANGES.md +53/−5
- cryptol.cabal +3/−2
- cryptol/Main.hs +11/−5
- lib/Cryptol.cry +2/−2
- src/Cryptol/Eval/FFI.hs +1/−1
- src/Cryptol/Eval/Generic.hs +165/−39
- src/Cryptol/Eval/Reference.lhs +78/−26
- src/Cryptol/IR/Prove.hs +3/−2
- src/Cryptol/IR/TraverseNames.hs +1/−0
- src/Cryptol/ModuleSystem/Binds.hs +2/−2
- src/Cryptol/ModuleSystem/Name.hs +12/−17
- src/Cryptol/ModuleSystem/Names.hs +9/−6
- src/Cryptol/ModuleSystem/NamingEnv.hs +17/−11
- src/Cryptol/ModuleSystem/Renamer.hs +8/−4
- src/Cryptol/ModuleSystem/Renamer/Monad.hs +6/−3
- src/Cryptol/Parser.y +12/−4
- src/Cryptol/Parser/AST.hs +6/−2
- src/Cryptol/Parser/AST/Builder.hs +2/−0
- src/Cryptol/Parser/ExpandPropGuards.hs +3/−2
- src/Cryptol/Parser/Lexer.x +1/−0
- src/Cryptol/Parser/Name.hs +45/−11
- src/Cryptol/Parser/ParserUtils.hs +21/−21
- src/Cryptol/Parser/Token.hs +1/−0
- src/Cryptol/Project.hs +16/−5
- src/Cryptol/Project/Cache.hs +10/−2
- src/Cryptol/Project/Config.hs +11/−3
- src/Cryptol/Project/Monad.hs +1/−1
- src/Cryptol/REPL/Browse.hs +2/−3
- src/Cryptol/REPL/Command.hs +73/−56
- src/Cryptol/REPL/Monad.hs +13/−8
- src/Cryptol/Transform/MonoValues.hs +1/−1
- src/Cryptol/TypeCheck/Default.hs +26/−8
- src/Cryptol/TypeCheck/Error.hs +43/−7
- src/Cryptol/TypeCheck/InferTypes.hs +35/−1
- src/Cryptol/TypeCheck/Kind.hs +163/−15
- src/Cryptol/TypeCheck/ModuleInstance.hs +1/−0
- src/Cryptol/TypeCheck/Monad.hs +3/−3
- src/Cryptol/TypeCheck/SimpleSolver.hs +5/−1
- src/Cryptol/TypeCheck/Solve.hs +2/−0
- src/Cryptol/TypeCheck/Solver/Class.hs +26/−19
- src/Cryptol/TypeCheck/Solver/Improve.hs +16/−4
- src/Cryptol/TypeCheck/Solver/Types.hs +1/−1
- src/Cryptol/TypeCheck/Subst.hs +4/−236
- src/Cryptol/TypeCheck/Subst/Type.hs +293/−0
- src/Cryptol/TypeCheck/Type.hs +17/−4
- src/Cryptol/TypeCheck/TypePat.hs +4/−0
- src/Cryptol/Utils/Misc.hs +8/−0
CHANGES.md view
@@ -1,3 +1,51 @@+# 3.5.0 -- 2026-01-27++## Administrative changes++* The binary builds are now built with GHC 9.6 rather than 9.4.++## Language changes++* User-defined `newtype` and `enum` types can now derive instances for standard+ constraints like `Eq` and `Cmp`. This means you can use standard operations+ like `==` with your custom types. See the [manual+ section](https://galoisinc.github.io/cryptol/master/OverloadedOperations.html#derived-instances)+ for more information.++* The built-in types `Option` and `Result` now have derived instances for `Eq`,+ `Cmp`, and `SignedCmp`.++* We can now infer that `a = Bit`, from the constraint `Integral [n][a]`.++## Bug fixes++* Fix incorrect defaulting during type inference.+ ([#1957](https://github.com/GaloisInc/cryptol/issues/1957))++* Make comparison operators lazy so that they do not evaluate any more of the+ data structure than is required to determine the comparison result, matching+ the behavior of the reference evaluator.+ ([#1925](https://github.com/GaloisInc/cryptol/issues/1925))++* Modify project loading to update the cache after each module is validated,+ and make saving the cache atomic on file systems where renaming a file to+ an existing file is atomic. This is useful because we get partial results+ if the validation process is interrupted.+ +* Change the default behavior of `-p`/`--project`. The new behavior is that+ it will check all files that have changed, and also files that have not+ been previously verified. The old behavior would only validate files that+ have changed since last time.++* Add a new flag, `--modified-project` which gives us the old `-p` behavior+ (i.e., check only files that have changed).++* Replace the `--untested-project` flag with the `--unsuccessful-project` flag.+ This will run validation on all files that have not been successfully validated,+ including ones that perviously failed, and have not changed.++* Allow user to specify how many satisfying results `satProve` (from `IR/Prove.hs`) produces+ # 3.4.0 -- 2025-11-07 ## Language changes@@ -6,7 +54,7 @@ without an explicit argument, we now run only the properties in the currently *focused module*. This is a change in behavior, because previously we used to run all properties in the currently opened *file*. This change- is only noticable when working with nested modules. The new behavior works+ is only noticeable when working with nested modules. The new behavior works better when these commands are used from docstrings (e.g., with the new behavior, writing `:check` on a submodule, will only check the properties in that submodule, as expected). @@ -36,7 +84,7 @@ ## Bug fixes -* Fix a discrepency between the behavior of `:check-docstrings` when run+* Fix a discrepancy between the behavior of `:check-docstrings` when run on the REPL vs. when run with a project. ([#1903](https://github.com/GaloisInc/cryptol/issues/1903)) @@ -289,7 +337,7 @@ * Add `:new-seed` and `:set-seed` commands to the REPL. These affect random test generation,- and help write reproducable Cryptol scripts.+ and help write reproducible Cryptol scripts. * Add support for the CVC5 solver, which can be selected with `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can@@ -345,7 +393,7 @@ * "Type mismatch" errors now show a context giving more information about the location of the error. The context is shown when the part of the types match, but then some nested types do not.- For example, when mathching `{ a : [8], b : [8] }` with+ For example, when matching `{ a : [8], b : [8] }` with `{ a : [8], b : [16] }` the error will be `8` does not match `16` and the context will be `{ b : [ERROR] _ }` indicating that the error is in the length of the sequence of field `b`.@@ -457,7 +505,7 @@ ## Language changes * The `newtype` construct, which has existed in the interpreter in an- incomplete and undocumented form for quite a while, is now fullly+ incomplete and undocumented form for quite a while, is now fully supported. The construct is documented in section 1.22 of [Programming Cryptol](https://cryptol.net/files/ProgrammingCryptol.pdf). Note, however, that the `cryptol-remote-api` RPC server currently does not
cryptol.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: cryptol-Version: 3.4.0+Version: 3.5.0 Synopsis: Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License: BSD-3-Clause@@ -29,7 +29,7 @@ type: git location: https://github.com/GaloisInc/cryptol.git -- add a tag on release branches- tag: 3.4.0+ tag: 3.5.0 flag static@@ -174,6 +174,7 @@ Cryptol.TypeCheck.Error, Cryptol.TypeCheck.Kind, Cryptol.TypeCheck.Subst,+ Cryptol.TypeCheck.Subst.Type, Cryptol.TypeCheck.Instantiate, Cryptol.TypeCheck.Unify, Cryptol.TypeCheck.PP,
cryptol/Main.hs view
@@ -68,7 +68,7 @@ , optHelp = False , optBatch = InteractiveRepl , optProject = Nothing- , optProjectRefresh = Project.ModifiedMode+ , optProjectRefresh = Project.UntestedMode Project.CachedFailed , optCallStacks = True , optCommands = [] , optColorMode = AutoColor@@ -93,9 +93,12 @@ , Option "" ["refresh-project"] (NoArg setProjectRefresh) "Ignore a pre-existing cache file when loading a project." - , Option "" ["untested-project"] (NoArg setProjectUntested)- "Load all project files that don't have a test result."+ , Option "" ["unsuccessful-project"] (NoArg setProjectUnsuccessful)+ "Load all project files that don't have a successful test result." + , Option "" ["modified-project"] (NoArg setProjectModified)+ "Load all project files that have been modified."+ , Option "e" ["stop-on-error"] (NoArg setStopOnError) "stop script execution as soon as an error occurs." @@ -160,8 +163,11 @@ setProjectRefresh :: OptParser Options setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = Project.RefreshMode } -setProjectUntested :: OptParser Options-setProjectUntested = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode }+setProjectUnsuccessful :: OptParser Options+setProjectUnsuccessful = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode Project.RecheckFailed }++setProjectModified :: OptParser Options+setProjectModified = modify $ \opts -> opts { optProjectRefresh = Project.ModifiedMode } -- | Set the color mode of the terminal output. setColorMode :: String -> OptParser Options
lib/Cryptol.cry view
@@ -642,7 +642,7 @@ * functions, i.e., functions that are not defined over their entire input * range. In these situations, 'None' can be used as a placeholder return value. */-enum Option a = None | Some a+enum Option a = None | Some a deriving (Eq, Cmp, SignedCmp) /** * Values of the 'Result t e' type can either be 'Ok', representing success and@@ -651,7 +651,7 @@ * expected and recoverable. For instance, 'e' might be a 'String' with an error * message, or it might be an 'Integer' with an error code. */-enum Result t e = Ok t | Err e+enum Result t e = Ok t | Err e deriving (Eq, Cmp, SignedCmp) // Bit specific operations ----------------------------------------
src/Cryptol/Eval/FFI.hs view
@@ -20,7 +20,7 @@ import Cryptol.Eval.FFI.Error ( FFILoadError ) import Cryptol.Eval (Eval, EvalEnv ) import Cryptol.TypeCheck.AST- ( Name, FFI(..), TVar(TVBound), findForeignDecls )+ ( FFI(..), TVar(TVBound), findForeignDecls ) import Cryptol.TypeCheck.FFI.FFIType ( FFIFunType(..) ) #ifdef FFI_ENABLED
src/Cryptol/Eval/Generic.hs view
@@ -31,10 +31,13 @@ import System.Random.TF.Gen (seedTFGen) import Data.Bits ((.&.), shiftR)+import Data.Foldable import Data.Maybe (fromMaybe) import qualified Data.Map.Strict as Map import Data.Map(Map)+import qualified Data.IntMap.Strict as IMap import Data.Ratio ((%))+import qualified Data.Vector as Vector import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd)@@ -247,14 +250,21 @@ -- records TVRec fs ->+ doRecord fs++ TVNominal _ _ ntv ->+ case ntv of+ -- newtypes+ TVStruct fs -> doRecord fs+ _ -> evalPanic "ringBinary" ["Enum/Abstract type not in `Ring`"]++ where+ doRecord fs = do VRecord <$> traverseRecordMap (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r))) fs - TVNominal {} ->- evalPanic "ringBinary" ["Nominal type not in `Ring`"]- type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym) @@ -326,14 +336,22 @@ -- records TVRec fs ->+ doRecord fs++ TVNominal _ _ ntv ->+ case ntv of+ -- newtypes+ TVStruct fs -> doRecord fs+ _ -> evalPanic "ringUnary" ["Enum/Abstract type not in `Ring`"]++ where+ doRecord fs = VRecord <$> traverseRecordMap (\f fty -> sDelay sym (loop' fty (lookupRecord f v))) fs - TVNominal {} -> evalPanic "ringUnary" ["Nominal type not in `Ring`"] - {-# SPECIALIZE ringNullary :: Concrete -> (Integer -> SEval Concrete (SWord Concrete)) ->@@ -393,12 +411,18 @@ do xs <- mapM (sDelay sym . loop) tys pure $ VTuple xs - TVRec fs ->+ TVRec fs -> doRecord fs++ TVNominal _ _ ntv ->+ case ntv of+ TVStruct fs -> doRecord fs+ _ -> evalPanic "ringNullary" ["Enum/Abstract type not in `Ring`"]++ where+ doRecord fs = do xs <- traverse (sDelay sym . loop) fs pure $ VRecord xs - TVNominal {} ->- evalPanic "ringNullary" ["Nominal type not in `Ring`"] {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete -> (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->@@ -725,26 +749,30 @@ {-# SPECIALIZE cmpValue :: Concrete ->+ (SBit Concrete -> a -> a -> SEval Concrete a) -> (SBit Concrete -> SBit Concrete -> SEval Concrete a -> SEval Concrete a) -> (SWord Concrete -> SWord Concrete -> SEval Concrete a -> SEval Concrete a) -> (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) -> (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) -> (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) -> (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->+ (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) -> (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a) #-} cmpValue :: Backend sym => sym ->+ (SBit sym -> a -> a -> SEval sym a) -> -- ^ how to merge @a@s based on a condition (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) -> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) -> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) -> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->+ (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> -- ^ how to compare enum tags (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)-cmpValue sym fb fw fi fz fq ff = cmp+cmpValue sym merge fb fw fi fz fq ff ftag = cmp where cmp ty v1 v2 k = case ty of@@ -753,8 +781,8 @@ TVFloat _ _ -> ff (fromVFloat v1) (fromVFloat v2) k TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k TVRational -> fq (fromVRational v1) (fromVRational v2) k- TVArray{} -> panic "Cryptol.Prims.Value.cmpValue"- [ "Arrays are not comparable" ]+ TVArray{} -> evalPanic "Cryptol.Eval.Generic.cmpValue"+ [ "Arrays are not comparable" ] TVSeq n t | isTBit t -> do w1 <- fromVWord sym "cmpValue" v1 w2 <- fromVWord sym "cmpValue" v2@@ -763,20 +791,82 @@ (enumerateSeqMap n (fromVSeq v1)) (enumerateSeqMap n (fromVSeq v2)) k- TVStream _ -> panic "Cryptol.Prims.Value.cmpValue"- [ "Infinite streams are not comparable" ]- TVFun _ _ -> panic "Cryptol.Prims.Value.cmpValue"- [ "Functions are not comparable" ]+ TVStream _ -> evalPanic "Cryptol.Eval.Generic.cmpValue"+ [ "Infinite streams are not comparable" ]+ TVFun _ _ -> evalPanic "Cryptol.Eval.Generic.cmpValue"+ [ "Functions are not comparable" ] TVTuple tys -> cmpValues tys (fromVTuple v1) (fromVTuple v2) k- TVRec fields -> cmpValues- (recordElements fields)- (recordElements (fromVRecord v1))- (recordElements (fromVRecord v2))- k+ TVRec fields -> cmpRecord fields - TVNominal {} -> evalPanic "cmpValue"- [ "Nominal type not in `Cmp`" ]+ TVNominal _ _ ntv ->+ case ntv of+ TVStruct fields -> cmpRecord fields+ TVEnum conTypes -> cmpEnum conTypes+ TVAbstract -> evalPanic "Cryptol.Eval.Generic.cmpValue"+ [ "Abstract types are not comparable" ] + where+ cmpRecord fields = cmpValues+ (recordElements fields)+ (recordElements (fromVRecord v1))+ (recordElements (fromVRecord v2))+ k++ cmpEnum conTypes = do+ let (tag1, cons1) = fromVEnum v1+ (tag2, cons2) = fromVEnum v2+ -- first compare based on tag...+ ftag tag1 tag2+ -- if both tags are concrete...+ case (integerAsLit sym tag1, integerAsLit sym tag2) of+ (Just i, Just j)+ -- ...then because the comparisons are lazy, this part should+ -- only be evaluated if tag1 == tag2+ | i == j -> do+ -- in the fully concrete case, just look up the fields for+ -- this constructor and compare them+ let i' = fromInteger i+ case (IMap.lookup i' cons1, IMap.lookup i' cons2) of+ (Just con1, Just con2) -> cmpFields i' con1 con2+ _ -> evalPanic "Cryptol.Eval.Generic.cmpValue"+ ["Missing constructor for tag", show i']+ | otherwise ->+ evalPanic "Cryptol.Eval.Generic.cmpValue"+ [ "Concrete enum tags not equal in equal case"+ , "Comparisons not lazy enough?" ]+ _ -> do+ -- in the symbolic case, here tag1 may or may not equal tag2, so+ -- we need to explicitly check this+ sameTag <- intEq sym tag1 tag2+ -- if tag1 == tag2, then compare by field, otherwise we are done+ -- comparing+ mergeEval sym merge sameTag doFields k+ where+ doFields =+ -- build up an if-then-else chain for each possible tag+ -- value+ IMap.foldrWithKey doFieldsForTag notFound $+ -- since at this point we know tag1 == tag2, we only need+ -- to consider the intersection of their possible+ -- constructors+ IMap.intersectionWith (,) cons1 cons2+ doFieldsForTag i (con1, con2) doRest = do+ -- if the tag is i, then compare fields for constructor i+ i' <- integerLit sym (toInteger i)+ -- we know tag1 == tag2, so we arbitrarily use tag1 here+ isThisTag <- intEq sym tag1 i'+ mergeEval sym merge isThisTag+ (cmpFields i con1 con2)+ doRest+ notFound = raiseError sym $ NoMatchingConstructor Nothing+ where+ cmpFields i con1 con2 =+ cmpValues+ (toList (conFields (conTypes Vector.! i)))+ (toList (conFields con1))+ (toList (conFields con2))+ k+ cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k = do x1' <- x1 x2' <- x2@@ -796,7 +886,7 @@ {-# INLINE valEq #-} valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)-valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)+valEq sym ty v1 v2 = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure $ bitLit sym True) where fb x y k = eqCombine sym (bitEq sym x y) k fw x y k = eqCombine sym (wordEq sym x y) k@@ -804,11 +894,12 @@ fz m x y k = eqCombine sym (znEq sym m x y) k fq x y k = eqCombine sym (rationalEq sym x y) k ff x y k = eqCombine sym (fpEq sym x y) k+ ftag = fi {-# INLINE valLt #-} valLt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)-valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)+valLt sym ty v1 v2 final = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure final) where fb x y k = lexCombine sym (bitLessThan sym x y) (bitEq sym x y) k fw x y k = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k@@ -816,11 +907,12 @@ fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"] fq x y k = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k ff x y k = lexCombine sym (fpLessThan sym x y) (fpEq sym x y) k+ ftag = fi {-# INLINE valGt #-} valGt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)-valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)+valGt sym ty v1 v2 final = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure final) where fb x y k = lexCombine sym (bitGreaterThan sym x y) (bitEq sym x y) k fw x y k = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k@@ -828,6 +920,7 @@ fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"] fq x y k = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k ff x y k = lexCombine sym (fpGreaterThan sym x y) (fpEq sym x y) k+ ftag = fi {-# INLINE eqCombine #-} eqCombine :: Backend sym =>@@ -835,7 +928,12 @@ SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym)-eqCombine sym eq k = join (bitAnd sym <$> eq <*> k)+eqCombine sym eq k =+ do e <- eq+ -- lazy `and` operator+ case bitAsLit sym e of+ Just False -> pure e+ _ -> bitAnd sym e =<< k {-# INLINE lexCombine #-} lexCombine :: Backend sym =>@@ -846,8 +944,15 @@ SEval sym (SBit sym) lexCombine sym cmp eq k = do c <- cmp- e <- eq- bitOr sym c =<< bitAnd sym e =<< k+ -- lazy `or` operator+ case bitAsLit sym c of+ Just True -> pure c+ _ ->+ do e <- eq+ -- lazy `and` operator+ case bitAsLit sym e of+ Just False -> pure c+ _ -> bitOr sym c =<< bitAnd sym e =<< k {-# INLINE eqV #-} eqV :: Backend sym => sym -> Binary sym@@ -875,7 +980,8 @@ {-# INLINE signedLessThanV #-} signedLessThanV :: Backend sym => sym -> Binary sym-signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)+signedLessThanV sym ty v1 v2 =+ VBit <$> cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure $ bitLit sym False) where fb _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"] fw x y k = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k@@ -883,6 +989,7 @@ fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"] fq _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"] ff _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]+ ftag x y k = lexCombine sym (intLessThan sym x y) (intEq sym x y) k @@ -942,11 +1049,18 @@ -- records TVRec fields ->- do xs <- traverse (sDelay sym . zeroV sym) fields- pure $ VRecord xs+ doRecord fields - TVNominal {} -> evalPanic "zeroV" [ "Nominal type not in `Zero`" ]+ -- newtypes+ TVNominal _ _ ntv ->+ case ntv of+ TVStruct fields -> doRecord fields+ _ -> evalPanic "zeroV" [ "Enum/Abstract type not in `Zero`" ] + where+ doRecord fields =+ do xs <- traverse (sDelay sym . zeroV sym) fields+ pure $ VRecord xs {-# SPECIALIZE joinSeq :: Concrete ->@@ -1289,15 +1403,21 @@ TVFun _ bty -> lam sym $ \ a -> loop' bty (fromVFun sym l a) (fromVFun sym r a) - TVRec fields ->+ TVRec fields -> doRecord fields++ TVNominal _ _ ntv ->+ case ntv of+ TVStruct fields -> doRecord fields+ _ -> evalPanic "logicBinary"+ [ "Enum/Abstract type not in `Logic`" ]++ where+ doRecord fields = VRecord <$> traverseRecordMap (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r))) fields - TVNominal {} -> evalPanic "logicBinary"- [ "Nominal type not in `Logic`" ]- {-# SPECIALIZE logicUnary :: Concrete -> (SBit Concrete -> SEval Concrete (SBit Concrete)) ->@@ -1346,13 +1466,19 @@ TVFun _ bty -> lam sym $ \ a -> loop' bty (fromVFun sym val a) - TVRec fields ->+ TVRec fields -> doRecord fields++ TVNominal _ _ ntv ->+ case ntv of+ TVStruct fields -> doRecord fields+ _ -> evalPanic "logicUnary" [ "Enum/Abstract type not in `Logic`" ]++ where+ doRecord fields = VRecord <$> traverseRecordMap (\f fty -> sDelay sym (loop' fty (lookupRecord f val))) fields-- TVNominal {} -> evalPanic "logicUnary" [ "Nominal type not in `Logic`" ] {-# INLINE assertIndexInBounds #-}
src/Cryptol/Eval/Reference.lhs view
@@ -35,6 +35,8 @@ > import qualified LibBF as FP > import qualified GHC.Num.Compat as Integer > import qualified Data.List as List+> import Data.Vector (Vector)+> import qualified Data.Vector as Vector > > import Cryptol.ModuleSystem.Name (asPrim,nameIdent) > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)@@ -43,7 +45,7 @@ > import qualified Cryptol.Backend.FloatHelpers as FP > import Cryptol.Backend.Monad (EvalError(..)) > import Cryptol.Eval.Type-> (TValue(..), TNominalTypeValue(..),+> (TValue(..), TNominalTypeValue(..), ConInfo(..), > isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar) > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2) > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim, unpackIdent)@@ -1076,9 +1078,9 @@ a zero value for all the built-in types for Cryptol. For bits, bitvectors and the base numeric types, this returns the obvious 0 representation. For sequences, records,-and tuples, the zero method operates pointwise the underlying types.-For functions, `zero` returns the constant function that returns-`zero` in the codomain.+tuples, and newtypes deriving `Zero`, the zero method operates+pointwise the underlying types. For functions, `zero` returns+the constant function that returns `zero` in the codomain. > zero :: TValue -> Value > zero TVBit = VBit False@@ -1093,7 +1095,10 @@ > zero (TVRec fields) = VRecord [ (f, pure (zero fty)) > | (f, fty) <- canonicalFields fields ] > zero (TVFun _ bty) = VFun (\_ -> pure (zero bty))-> zero (TVNominal {}) = evalPanic "zero" ["Nominal type not in `Zero`"]+> zero (TVNominal _ _ ntv) =+> case ntv of+> TVStruct fields -> zero (TVRec fields)+> _ -> evalPanic "zero" ["Enum/Abstract type not in `Zero`"] Literals --------@@ -1162,7 +1167,10 @@ > TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"] > TVRational -> evalPanic "logicUnary" ["Rational not in class Logic"] > TVFloat{} -> evalPanic "logicUnary" ["Float not in class Logic"]-> TVNominal {} -> evalPanic "logicUnary" ["Nominal type not in `Logic`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fields -> go (TVRec fields) val+> _ -> evalPanic "logicUnary" ["Enum/Abstract type not in `Logic`"] > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value > logicBinary op = go@@ -1200,7 +1208,10 @@ > TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"] > TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"] > TVFloat{} -> evalPanic "logicBinary" ["Float not in class Logic"]-> TVNominal {} -> evalPanic "logicBinary" ["Nominal type not in `Logic`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fields -> go (TVRec fields) l r+> _ -> evalPanic "logicBinary" ["Enum/Abstract type not in `Logic`"] Ring Arithmetic@@ -1224,7 +1235,7 @@ > go ty = > case ty of > TVBit ->-> evalPanic "arithNullary" ["Bit not in class Ring"]+> evalPanic "ringNullary" ["Bit not in class Ring"] > TVInteger -> > VInteger <$> i > TVIntMod n ->@@ -1234,7 +1245,7 @@ > TVFloat e p -> > VFloat . fpToBF e p <$> fl e p > TVArray{} ->-> evalPanic "arithNullary" ["Array not in class Ring"]+> evalPanic "ringNullary" ["Array not in class Ring"] > TVSeq w a > | isTBit a -> vWord w <$> i > | otherwise -> pure $ VList (Nat w) (genericReplicate w (go a))@@ -1246,8 +1257,10 @@ > pure $ VTuple (map go tys) > TVRec fs -> > pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ]-> TVNominal {} ->-> evalPanic "arithNullary" ["Newtype type not in `Ring`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fs -> go (TVRec fs)+> _ -> evalPanic "ringNullary" ["Enum/Abstract type not in `Ring`"] > ringUnary :: > (Integer -> E Integer) ->@@ -1260,11 +1273,11 @@ > go ty val = > case ty of > TVBit ->-> evalPanic "arithUnary" ["Bit not in class Ring"]+> evalPanic "ringUnary" ["Bit not in class Ring"] > TVInteger -> > VInteger <$> appOp1 iop (fromVInteger <$> val) > TVArray{} ->-> evalPanic "arithUnary" ["Array not in class Ring"]+> evalPanic "ringUnary" ["Array not in class Ring"] > TVIntMod n -> > VInteger <$> appOp1 (\i -> flip mod n <$> iop i) (fromVInteger <$> val) > TVRational ->@@ -1284,8 +1297,10 @@ > do val' <- val > pure $ VRecord [ (f, go fty (lookupRecord f val')) > | (f, fty) <- canonicalFields fs ]-> TVNominal {} ->-> evalPanic "arithUnary" ["Nominal type not in `Ring`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fs -> go (TVRec fs) val+> _ -> evalPanic "ringUnary" ["Enum/Abstract type not in `Ring`"] > ringBinary :: > (Integer -> Integer -> E Integer) ->@@ -1298,7 +1313,7 @@ > go ty l r = > case ty of > TVBit ->-> evalPanic "arithBinary" ["Bit not in class Ring"]+> evalPanic "ringBinary" ["Bit not in class Ring"] > TVInteger -> > VInteger <$> appOp2 iop (fromVInteger <$> l) (fromVInteger <$> r) > TVIntMod n ->@@ -1309,7 +1324,7 @@ > VFloat . fpToBF e p <$> > appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r) > TVArray{} ->-> evalPanic "arithBinary" ["Array not in class Ring"]+> evalPanic "ringBinary" ["Array not in class Ring"] > TVSeq w a > | isTBit a -> vWord w <$> appOp2 iop (fromVWord =<< l) (fromVWord =<< r) > | otherwise ->@@ -1332,8 +1347,10 @@ > pure $ VRecord > [ (f, go fty (lookupRecord f l') (lookupRecord f r')) > | (f, fty) <- canonicalFields fs ]-> TVNominal {} ->-> evalPanic "arithBinary" ["Nominal type not in class `Ring`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fs -> go (TVRec fs) l r+> _ -> evalPanic "ringBinary" ["Enum/Abstract type not in class `Ring`"] Integral@@ -1463,12 +1480,16 @@ Comparison ---------- -Comparison primitives may be applied to any type that is constructed of-out of base types and tuples, records and finite sequences.+Comparison primitives may be applied to any type that is constructed+out of base types and tuples, records, finite sequences, and newtypes+and enums deriving the appropriate instances. All such types are compared using a lexicographic ordering of components. On bits, we have `False` < `True`. Sequences and tuples are compared left-to-right, and record fields are compared in-alphabetical order.+alphabetical order. Newtypes are compared using their underlying records.+Enums are compared first based on constructor, in the order that they are+listed in the `enum` declaration, then for enum values with the same+constructor, by the constructor fields in left-to-right order. Comparisons on base types are strict in both arguments. Comparisons on larger types have short-circuiting behavior: A comparison involving an@@ -1510,8 +1531,12 @@ > ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l > rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r > lexList (zipWith3 lexCompare tys ls rs)-> TVNominal {} ->-> evalPanic "lexCompare" ["Nominal type not in `Cmp`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fields -> lexCompare (TVRec fields) l r+> TVEnum conInfos -> lexEnum lexCompare conInfos l r+> TVAbstract ->+> evalPanic "lexCompare" ["Abstract type not in `Cmp`"] > > lexList :: [E Ordering] -> E Ordering > lexList [] = pure EQ@@ -1520,6 +1545,29 @@ > LT -> pure LT > EQ -> lexList es > GT -> pure GT+>+> -- | Lexicographic ordering on enums, given a comparison function for fields.+> lexEnum :: (TValue -> E Value -> E Value -> E Ordering)+> -> Vector (ConInfo TValue) -> E Value -> E Value -> E Ordering+> lexEnum cmp conInfos l r =+> do (lcon, lfields) <- fromVEnum <$> l+> (rcon, rfields) <- fromVEnum <$> r+> let lconIndex = conIndex lcon+> rconIndex = conIndex rcon+> -- We arbitrarily use the field types of the left side constructor+> -- here, but this is okay since this should only be evaluated when+> -- the left and right constructors are the same.+> fieldTys = Vector.toList $+> conFields (conInfos Vector.! lconIndex)+> lexList (pure (compare lconIndex rconIndex)+> : zipWith3 cmp fieldTys lfields rfields)+> where+> conIndex con =+> case Vector.findIndex ((== con) . conIdent) conInfos of+> Just i -> i+> Nothing ->+> evalPanic "lexEnum"+> ["Unknown enum constructor " ++ unpackIdent con] Signed comparisons may be applied to any type made up of non-empty bitvectors using finite sequences, tuples and records.@@ -1564,8 +1612,12 @@ > ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l > rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r > lexList (zipWith3 lexSignedCompare tys ls rs)-> TVNominal {} ->-> evalPanic "lexSignedCompare" ["Nominal type not in `Cmp`"]+> TVNominal _ _ ntv ->+> case ntv of+> TVStruct fields -> lexSignedCompare (TVRec fields) l r+> TVEnum conInfos -> lexEnum lexSignedCompare conInfos l r+> TVAbstract ->+> evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"] Sequences
src/Cryptol/IR/Prove.hs view
@@ -29,16 +29,17 @@ [DeclGroup] {-^ Additional definitions -} -> Expr {-^ The expression we are examining -} -> Type {-^ The type of the expression to examine -} ->+ Int {-^ How many satisfying assumptions produced -} -> Int {-^ Timeout in seconds -} -> ModuleM [SatResult] {- ^ A list of possible models (lazy). Empty if no models were found. -}-satProve decls expr exprType timeoutSec =+satProve decls expr exprType numResults timeoutSec = do timing <- M.io (newIORef 0) let cmd = ProverCommand {- pcQueryType = SatQuery AllSat,+ pcQueryType = SatQuery (SomeSat numResults), pcProverName = "z3", pcVerbose = False, pcValidate = True,
src/Cryptol/IR/TraverseNames.hs view
@@ -214,6 +214,7 @@ <*> pure (ntKind nt) <*> traverseNamesIP (ntConstraints nt) <*> traverseNamesIP (ntDef nt)+ <*> traverse traverseNamesIP (ntDeriving nt) <*> pure (ntFixity nt) <*> pure (ntDoc nt)
src/Cryptol/ModuleSystem/Binds.hs view
@@ -31,7 +31,7 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident(allNamespaces) import Cryptol.Parser.Position-import Cryptol.Parser.Name(isGeneratedName)+import Cryptol.Parser.Name(isSystemName) import Cryptol.Parser.AST import Cryptol.ModuleSystem.Exports(exportedDecls,exported) import Cryptol.ModuleSystem.Renamer.Error@@ -434,7 +434,7 @@ FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name newTop ns m thing fx rng = liftSupply (mkDeclared ns m src (getIdent thing) fx rng)- where src = if isGeneratedName thing then SystemName else UserName+ where src = if isSystemName thing then SystemName else UserName newLocal :: FreshM m => Namespace -> PName -> Range -> m Name newLocal ns thing rng = liftSupply (mkLocalPName ns thing rng)
src/Cryptol/ModuleSystem/Name.hs view
@@ -20,8 +20,7 @@ module Cryptol.ModuleSystem.Name ( -- * Names- Name(), NameInfo(..)- , NameSource(..)+ Name(), NameInfo(..), NameSource(..) , nameUnique , nameIdent , mapNameIdent@@ -74,7 +73,7 @@ import Data.Char(isAlpha,toUpper) -import Cryptol.Parser.Name (PName)+import Cryptol.Parser.Name (PName, NameSource(..)) import qualified Cryptol.Parser.Name as PName import Cryptol.Parser.Position (Range,Located(..)) import Cryptol.Utils.Fixity@@ -104,10 +103,6 @@ } deriving (Generic, NFData, Show) -data NameSource = SystemName | UserName- deriving (Generic, NFData, Show, Eq)-- instance Eq Name where a == b = compare a b == EQ a /= b = compare a b /= EQ@@ -244,22 +239,22 @@ nameToDefPName :: Name -> PName nameToDefPName n = case nInfo n of- GlobalName _ og -> PName.origNameToDefPName og- LocalName _ _ txt -> PName.mkUnqual txt+ GlobalName ns og -> PName.origNameToDefPName og ns+ LocalName ns _ txt -> PName.UnQual' txt ns -- | Compute a `PName` from `Name`, this preserves all qualifiers in the name, -- whereas `nameToDefPName` does not. nameToPNameWithQualifiers :: Name -> PName nameToPNameWithQualifiers n = case nameInfo n of- GlobalName _ og -> origNameToPName og- LocalName _ _ txt -> PName.mkUnqual txt+ GlobalName ns og -> origNameToPName og ns+ LocalName ns _ txt -> PName.UnQual' txt ns where- origNameToPName :: OrigName -> PName- origNameToPName og =+ origNameToPName :: OrigName -> NameSource -> PName+ origNameToPName og vis = case modPathSplit (ogModule og) of- (_top,[] ) -> PName.UnQual ident+ (_top,[] ) -> PName.UnQual' ident vis (_top,ids) -> PName.Qual (packModName (map identText ids)) ident where@@ -419,8 +414,8 @@ where ident = PName.getIdent nm src = case nm of- PName.NewName {} -> SystemName- _ -> UserName+ PName.NewName {} -> PName.SystemName+ _ -> PName.UserName -- | Make a new parameter name. mkLocal :: NameSource -> Namespace -> Ident -> Range -> Supply -> (Name,Supply)@@ -453,7 +448,7 @@ (u,s') = nextUnique s name = Name { nUnique = u , nInfo = GlobalName- UserName+ PName.UserName OrigName { ogModule = own , ogName = nameIdent n
src/Cryptol/ModuleSystem/Names.hs view
@@ -23,16 +23,20 @@ One x -> [x] Ambig ns -> Set.toList ns +-- | Returns a UserName if one is available, otherwise it returns+-- | a SystemName. anyOne :: Names -> Name anyOne xs = case xs of One x -> x Ambig ns- | Set.null ns- -> panic "anyOne" ["Ambig with no names"]- | otherwise- -> Set.elemAt 0 ns-+ | Set.null ns ->+ panic "anyOne" ["Ambig with no names"]+ | Set.null l -> Set.elemAt 0 ns+ | otherwise -> Set.elemAt 0 l+ where+ l = Set.filter (\x -> nameSrc x == UserName) ns+ instance Semigroup Names where xs <> ys = case (xs,ys) of@@ -93,4 +97,3 @@ ys = case y of One z -> Set.delete z xs Ambig zs -> Set.difference xs zs-
src/Cryptol/ModuleSystem/NamingEnv.hs view
@@ -176,7 +176,7 @@ qualify pfx (NamingEnv env) = NamingEnv (Map.mapKeys toQual <$> env) where toQual (Qual mn n) = Qual (prependChunks pfx' mn) n- toQual (UnQual n) = Qual pfx n+ toQual (UnQual' n _ns) = Qual pfx n toQual n@NewName{} = n -- | prependChunks - add ChunksText to start of ModName@@ -214,14 +214,20 @@ NamingEnv ns = consToValues env -- | Get the subset of the first environment that shadows something--- in the second one.-findShadowing :: NamingEnv -> NamingEnv -> [ (PName,Name,[Name]) ]-findShadowing (NamingEnv lhs) rhs =- [ (p, anyOne xs, namesToList ys)- | (ns,mp) <- Map.toList lhs- , (p,xs) <- Map.toList mp- , Just ys <- [ lookupNS ns p rhs ]- ]+-- in the second one. We only consider UserNames in the second enviornment.+findShadowing :: NamingEnv -> NamingEnv -> [(PName, Name, [Name])]+findShadowing (NamingEnv lhs) rhs = res+ where+ res =+ [ (p, x, ysList)+ | (ns, mp) <- Map.toList lhs,+ (p, xs) <- Map.toList mp,+ let x = anyOne xs,+ Just ys <- [lookupNS ns p rhs],+ let ysList = filter isUser (namesToList ys),+ not (null ysList)+ ]+ isUser z = nameSrc z == UserName -- | Do an arbitrary choice for ambiguous names. -- We do this to continue checking afetr we've reported an ambiguity error.@@ -255,7 +261,7 @@ map fromTy (Map.elems mpnTypes)) ] where- toPName n = mkUnqual (nameIdent n)+ toPName n = UnQual' (nameIdent n) (nameSrc n) fromTy tp = let nm = T.mtpName tp in (toPName nm, One nm)@@ -276,7 +282,7 @@ unqualifiedEnv IfaceDecls { .. } = mconcat [ exprs, tySyns, ntTypes, ntExprs, mods, sigs ] where- toPName n = mkUnqual (nameIdent n)+ toPName n = UnQual' (nameIdent n) (nameSrc n) exprs = mconcat [ singletonNS NSValue (toPName n) n | n <- Map.keys ifDecls ]
src/Cryptol/ModuleSystem/Renamer.hs view
@@ -876,12 +876,14 @@ depsOf (NamedThing nameC) (addDep (thing nameT)) depsOf (NamedThing (thing nameT)) $- do ps' <- traverse rename (nParams n)- body' <- traverse (traverse rename) (nBody n)+ do ps' <- traverse rename (nParams n)+ body' <- traverse (traverse rename) (nBody n)+ deriving' <- traverse (rnLocated (renameType NameUse)) (nDeriving n) return Newtype { nName = nameT , nConName = nameC , nParams = ps'- , nBody = body' }+ , nBody = body'+ , nDeriving = deriving' } instance Rename EnumDecl where rename n =@@ -898,9 +900,11 @@ do ts' <- traverse rename (ecFields (tlValue tlEc)) let con = EnumCon { ecName = c, ecFields = ts' } pure tlEc { tlValue = con }+ deriving' <- traverse (rnLocated (renameType NameUse)) (eDeriving n) pure EnumDecl { eName = nameT , eParams = ps' , eCons = cons+ , eDeriving = deriving' } -- | Try to resolve a name.@@ -1120,7 +1124,7 @@ UpdFun -> UpdField UpdFun [l] <$> rename (EFun emptyFunDesc [PVar p] e) where- p = UnQual . selName <$> last ls+ p = mkUnqual . selName <$> last ls _ -> UpdField UpdFun [l] <$> rename (EUpd Nothing [ UpdField h more e]) [] -> panic "rename@UpdField" [ "Empty label list." ]
src/Cryptol/ModuleSystem/Renamer/Monad.hs view
@@ -350,11 +350,14 @@ pure (forceUnambig env) -- | Issue warnings if entries in the first environment would--- shadow something in the second.+-- shadow something in the second. This warning is only emited+-- for UserNames checkShadowing :: NamingEnv -> NamingEnv -> RenameM () checkShadowing envNew envOld =- mapM_ recordWarning- [ SymbolShadowed p x xs | (p,x,xs) <- findShadowing envNew envOld ]+ mapM_+ recordWarning+ [ SymbolShadowed p x xs | (p, x, xs) <- findShadowing envNew envOld+ ] -- | Shadow the current naming environment with some more names.
src/Cryptol/Parser.y view
@@ -9,6 +9,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE PatternSynonyms #-}+ module Cryptol.Parser ( parseModule , parseProgram, parseProgramWith@@ -39,6 +41,7 @@ import Cryptol.Parser.Token import Cryptol.Parser.ParserUtils import Cryptol.Parser.Unlit(PreProc(..), guessPreProc)+import Cryptol.Parser.Name (mkUnqual, pattern UnQual) import Cryptol.Utils.RecordMap(RecordMap) import Paths_cryptol@@ -69,6 +72,7 @@ 'type' { Located $$ (Token (KW KW_type ) _)} 'newtype' { Located $$ (Token (KW KW_newtype) _)} 'enum' { Located $$ (Token (KW KW_enum) _)}+ 'deriving' { Located $$ (Token (KW KW_deriving) _)} 'module' { Located $$ (Token (KW KW_module ) _)} 'submodule' { Located $$ (Token (KW KW_submodule ) _)} 'where' { Located $$ (Token (KW KW_where ) _)}@@ -442,16 +446,16 @@ : type {% mkPropGuards $1 } -newtype :: { Newtype PName }- : 'newtype' type '=' newtype_body {% mkNewtype $2 $4 }+newtype :: { Newtype PName }+ : 'newtype' type '=' newtype_body deriving {% mkNewtype $2 $4 $5 } newtype_body :: { Located (RecordMap Ident (Range, Type PName)) } : '{' '}' {% mkRecord (rComb $1 $2) (Located emptyRange) [] } | '{' field_types '}' {% mkRecord (rComb $1 $3) (Located emptyRange) $2 } -enum :: { EnumDecl PName }- : 'enum' type '=' enum_body {% mkEnumDecl $2 $4 }+enum :: { EnumDecl PName }+ : 'enum' type '=' enum_body deriving {% mkEnumDecl $2 $4 $5 } enum_body :: { [TopLevel (EnumCon PName)] } : enum_con { [$1] }@@ -461,6 +465,10 @@ enum_con :: { TopLevel (EnumCon PName) } : app_type {% mkConDecl Nothing Public $1 } | doc app_type {% mkConDecl (Just $1) Public $2 }++deriving :: { [Located PName] }+ : 'deriving' '(' vars_comma ')' { reverse $3 }+ | {- empty -} { [] } vars_comma :: { [ LPName ] } : var { [ $1] }
src/Cryptol/Parser/AST.hs view
@@ -154,7 +154,7 @@ newtype Program name = Program [TopDecl name] deriving (Show) -{- | A module for the pre-typechecker phasese. The two parameters are:+{- | A module for the pre-typechecker phases. The two parameters are: * @mname@ the type of module names. This is because top-level and nested modules use different types to identify a module.@@ -176,7 +176,7 @@ } deriving (Show, Generic, NFData) --- | Different flavours of module we have.+-- | Different flavours of modules we have. data ModuleDefinition name = NormalModule [TopDecl name] @@ -587,12 +587,14 @@ , nParams :: [TParam name] -- ^ Type params , nConName :: !name -- ^ Constructor function name , nBody :: Rec (Type name) -- ^ Body+ , nDeriving :: [Located name] -- ^ Derived typeclasses } deriving (Eq, Show, Generic, NFData) data EnumDecl name = EnumDecl { eName :: Located name -- ^ Type name , eParams :: [TParam name] -- ^ Type params , eCons :: [TopLevel (EnumCon name)] -- ^ Value constructors+ , eDeriving :: [Located name] -- ^ Derived typeclasses } deriving (Show, Generic, NFData) data EnumCon name = EnumCon@@ -1631,12 +1633,14 @@ , nParams = nParams n , nConName = nConName n , nBody = fmap noPos (nBody n)+ , nDeriving = map noPos (nDeriving n) } instance NoPos (EnumDecl name) where noPos n = EnumDecl { eName = noPos (eName n) , eParams = eParams n , eCons = map noPos (eCons n)+ , eDeriving = map noPos (eDeriving n) } instance NoPos (EnumCon name) where
src/Cryptol/Parser/AST/Builder.hs view
@@ -58,6 +58,8 @@ funT2 f a b = var f $^ [PosInst a, PosInst b] -- | Create an unqualified variable expression from an identifier.+-- We assume here that the variable's PName is user visible, i.e. +-- is a UserName var :: Ident -> Expr PName var = EVar . mkUnqual
src/Cryptol/Parser/ExpandPropGuards.hs view
@@ -27,6 +27,7 @@ import Data.Foldable (traverse_) import Data.Text (pack) import GHC.Generics (Generic)+import Cryptol.Parser.Name (NameSource(SystemName)) -- | Monad type ExpandPropGuardsM a = Either Error a@@ -282,10 +283,10 @@ let txt = identText ident txt' = pack $ show $ pp props in Qual modName (mkIdent $ txt <> txt') <$ locName- UnQual ident ->+ UnQual' ident _ns -> let txt = identText ident txt' = pack $ show $ pp props- in UnQual (mkIdent $ txt <> txt') <$ locName+ in UnQual' (mkIdent $ txt <> txt') SystemName <$ locName NewName _ _ -> panic "mkName" [ "During expanding prop guards"
src/Cryptol/Parser/Lexer.x view
@@ -108,6 +108,7 @@ "interface" { emit $ KW KW_interface } "newtype" { emit $ KW KW_newtype } "enum" { emit $ KW KW_enum }+"deriving" { emit $ KW KW_deriving } "pragma" { emit $ KW KW_pragma } "property" { emit $ KW KW_property } "then" { emit $ KW KW_then }
src/Cryptol/Parser/Name.hs view
@@ -8,8 +8,21 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE Safe #-}+{-# LANGUAGE PatternSynonyms #-} -module Cryptol.Parser.Name where+module Cryptol.Parser.Name (+ NameSource(..)+ , PName(..)+ , Pass(..)+ , mkQual+ , mkUnqual+ , mkUnqualSystem+ , origNameToDefPName+ , getModName+ , getIdent+ , isSystemName+ , pattern UnQual+ ) where import Cryptol.Utils.Fixity import Cryptol.Utils.Ident@@ -22,8 +35,15 @@ -- Names ----------------------------------------------------------------------- +data NameSource = SystemName | UserName+ deriving (Generic, Show, Ord, Eq) -- | Names that originate in the parser.-data PName = UnQual !Ident+-- Note here that other kinds of PName do not need this kind of flag because: +-- (1) NewName are generated by the system, so these should never be user visible.+-- (2) Qual names are user names use to refer to imported modules. Should these names+-- names ever be used to refer to system names, then there make be a bug in the renamer+-- that needs to be fixed.+data PName = UnQual' !Ident !NameSource -- ^ Unqualified names like @x@, @Foo@, or @+@. | Qual !ModName !Ident -- ^ Qualified names like @Foo::bar@ or @module::!@.@@ -39,22 +59,31 @@ instance NFData PName instance NFData Pass+instance NFData NameSource +-- | Pattern synonym for when we are trying to deconstruct+-- unqualified PNames to get their identifiers.+pattern UnQual :: Ident -> PName+pattern UnQual i <- UnQual' i _+ mkUnqual :: Ident -> PName-mkUnqual = UnQual+mkUnqual = (`UnQual'` UserName) +mkUnqualSystem :: Ident -> PName+mkUnqualSystem = (`UnQual'` SystemName)+ mkQual :: ModName -> Ident -> PName mkQual = Qual -- | Compute a `PName` for the definition site corresponding to the given -- `OrigName`. Usually this is an unqualified name, but names that come -- from module parameters are qualified with the corresponding parameter name.-origNameToDefPName :: OrigName -> PName-origNameToDefPName og = toPName (ogName og)+origNameToDefPName :: OrigName -> NameSource -> PName+origNameToDefPName og vis = toPName (ogName og) where toPName = case ogFromParam og of- Nothing -> UnQual+ Nothing -> (`UnQual'` vis) Just sig -> Qual (identToModName sig) getModName :: PName -> Maybe ModName@@ -62,7 +91,7 @@ getModName _ = Nothing getIdent :: PName -> Ident-getIdent (UnQual n) = n+getIdent (UnQual' n _) = n getIdent (Qual _ n) = n getIdent (NewName p i) = packIdent ("__" ++ pass ++ show i) where@@ -71,11 +100,16 @@ MonoValues -> "mv" ExpandPropGuards _ -> "epg" -isGeneratedName :: PName -> Bool-isGeneratedName x =+++isSystemName :: PName -> Bool+isSystemName x = case x of- NewName {} -> True- _ -> False+ UnQual' _id ns -> case ns of+ SystemName -> True+ UserName -> False+ Qual _md _id -> False+ NewName _p _i -> True instance PP PName where ppPrec _ = ppPrefixName
src/Cryptol/Parser/ParserUtils.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE LambdaCase #-}@@ -55,6 +56,7 @@ import Cryptol.Utils.PP import Cryptol.Utils.Panic import Cryptol.Utils.RecordMap+import Cryptol.Parser.Name (pattern UnQual, mkUnqualSystem) parseString :: Config -> ParseM a -> String -> Either ParseError a@@ -195,14 +197,6 @@ expected x = P $ \cfg _ s -> Left (HappyUnexpected (cfgSource cfg) (sPrevTok s) x) -------- mkModName :: [Text] -> ModName mkModName = packModName @@ -222,7 +216,7 @@ $ modNameToNormalModName t ImpNested nm -> case nm of- UnQual i -> i+ UnQual' i _ -> i Qual _ i -> i NewName {} -> panic "mkModParamName" ["Unexpected NewName",show lsig] Just m -> packIdent (last (modNameChunks (thing m)))@@ -599,7 +593,6 @@ mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x) | otherwise = NamedInst x - mkTParam :: Located Ident -> Maybe Kind -> ParseM (TParam PName) mkTParam Located { srcRange = rng, thing = n } k | n == widthIdent = errorMessage rng ["`width` is not a valid type parameter name."]@@ -620,24 +613,27 @@ mkNewtype :: Type PName -> Located (RecordMap Ident (Range, Type PName)) ->+ [Located PName] -> ParseM (Newtype PName)-mkNewtype thead def =+mkNewtype thead def derivs = do (nm,params) <- typeToDecl thead- pure (Newtype nm params (thing nm) (thing def))+ pure (Newtype nm params (thing nm) (thing def) derivs) mkEnumDecl :: Type PName -> [ TopLevel (EnumCon PName) ] {- ^ Reversed -} ->+ [Located PName] -> ParseM (EnumDecl PName)-mkEnumDecl thead def =+mkEnumDecl thead def derivs = do (nm,params) <- typeToDecl thead mapM_ reportRepeated (Map.toList (Map.fromListWith (++) [ (thing k,[srcRange k]) | k <- map (ecName . tlValue) def ])) pure EnumDecl- { eName = nm- , eParams = params- , eCons = reverse def+ { eName = nm+ , eParams = params+ , eCons = reverse def+ , eDeriving = derivs } where reportRepeated (i,xs) =@@ -650,6 +646,7 @@ _ -> pure () +-- | This function handles constructor declarations mkConDecl :: Maybe (Located Text) -> ExportType -> Type PName -> ParseM (TopLevel (EnumCon PName))@@ -662,9 +659,9 @@ TLocated t1 r -> go (Just r) t1 TUser n ts -> case thing n of- UnQual i+ UnQual' i ns | isUpperIdent i ->- pure EnumCon { ecName = Located (srcRange n) (UnQual i)+ pure EnumCon { ecName = Located (srcRange n) (UnQual' i ns) , ecFields = ts } | otherwise ->@@ -1135,6 +1132,7 @@ , mDocTop = Nothing } +-- | Make a nested module, i.e. when you have a module inside a module. mkNested :: Module PName -> ParseM (NestedModule PName) mkNested m = case modNameChunks (thing nm) of@@ -1415,8 +1413,11 @@ AnonIfaceMod -> modNameIfaceMod toImpName = ImpTop +-- | Make anonymous names, i.e. a thing without a user visible name.+-- Anonymous names are used when we desugar some things related to the module system +-- (e.g. parameter blocks become interface modules). instance MkAnon PName where- mkAnon what = mkUnqual+ mkAnon what = mkUnqualSystem . case what of AnonArg l c -> const (identAnonArg l c) AnonIfaceMod -> identAnonIfaceMod@@ -1564,7 +1565,7 @@ origMod = iModule (thing i) iname = Located {- thing =mkUnqual+ thing = mkUnqualSystem $ let pos = from (srcRange i) in identAnonInstImport (line pos) (col pos), srcRange = srcRange origMod@@ -1580,6 +1581,5 @@ , tlDoc = Nothing , tlValue = NestedModule m }-
src/Cryptol/Parser/Token.hs view
@@ -37,6 +37,7 @@ | KW_submodule | KW_newtype | KW_enum+ | KW_deriving | KW_pragma | KW_property | KW_then
src/Cryptol/Project.hs view
@@ -8,6 +8,7 @@ , ChangeStatus(..) , InvalidStatus(..) , LoadProjectMode(..)+ , CheckFailedMode(..) , Parsed , loadProject , depMap@@ -46,12 +47,22 @@ untested (InFile f) = case out of Left _ -> True- Right m -> Map.lookup (CacheInFile f) m /= Just (Just True)+ Right m ->+ case mode of+ UntestedMode checkFailed ->+ case Map.lookup (CacheInFile f) m of+ Nothing -> True+ Just Nothing -> True+ Just (Just True) -> False+ Just (Just False) ->+ case checkFailed of+ RecheckFailed -> True+ CachedFailed -> False+ RefreshMode -> True+ ModifiedMode -> False - let needLoad = case mode of- RefreshMode -> [thing (P.mName m) | Scanned _ _ ps <- Map.elems statuses, (m, _) <- ps]- ModifiedMode -> [thing (P.mName m) | Scanned Changed _ ps <- Map.elems statuses, (m, _) <- ps]- UntestedMode -> [thing (P.mName m) | (k, Scanned ch _ ps) <- Map.assocs statuses, ch == Changed || untested k, (m, _) <- ps]+ let needLoad =+ [thing (P.mName m) | (k, Scanned ch _ ps) <- Map.assocs statuses, ch == Changed || untested k, (m, _) <- ps] let order = loadOrder deps needLoad let modDetails = Map.fromList [(thing (P.mName m), (m, mp, fp)) | (mp, Scanned _ fp ps) <- Map.assocs statuses, (m, _) <- ps]
src/Cryptol/Project/Cache.hs view
@@ -9,6 +9,7 @@ import qualified Data.ByteString as BS import Data.Set (Set) import System.Directory+import System.IO import System.FilePath as FP import System.IO.Error import qualified Toml@@ -102,7 +103,11 @@ data CacheEntry = CacheEntry { cacheFingerprint :: FullFingerprint+ -- ^ Identifier for a module that is part of the project+ , cacheDocstringResult :: Maybe Bool+ -- ^ `Nothing` means unchecked,+ -- `Just` means checked, and if validation succeeded. } deriving (Show, Read) @@ -126,7 +131,7 @@ emptyLoadCache :: LoadCache emptyLoadCache = LoadCache { cacheModules = mempty } --- | Load a cache. Also returns an id for the cahce.+-- | Load a cache. Also returns an id for the cache. -- If there is no cache (or it failed to load), then we return an empty id. loadLoadCache :: IO (LoadCache, CacheId) loadLoadCache =@@ -144,5 +149,8 @@ do createDirectoryIfMissing False metaDir let txt = Text.pack (show (Toml.encode cache)) !bytes = Text.encodeUtf8 txt- BS.writeFile loadCachePath bytes+ (tmpFile,h) <- openBinaryTempFile metaDir "load-cache-XXXXX.toml"+ BS.hPut h bytes+ hClose h+ renameFile tmpFile loadCachePath pure (SHA256.hash bytes)
src/Cryptol/Project/Config.hs view
@@ -22,9 +22,17 @@ } deriving Show data LoadProjectMode- = RefreshMode -- load all files- | ModifiedMode -- load modified files- | UntestedMode -- load files without a successful test result+ = RefreshMode + -- ^ load all files+ | ModifiedMode+ -- ^ load modified files+ | UntestedMode CheckFailedMode+ -- ^ load files without a successful test result+ deriving Show++-- | Indicates if we should load files that have not changed, but+-- contain failed properties.+data CheckFailedMode = RecheckFailed | CachedFailed deriving Show instance FromValue Config where
src/Cryptol/Project/Monad.hs view
@@ -148,7 +148,7 @@ (cache,cacheId) <- case mode of RefreshMode -> pure (emptyLoadCache, emptyCacheId)- UntestedMode -> loadLoadCache+ UntestedMode _ -> loadLoadCache ModifiedMode -> loadLoadCache pure LoadConfig { canonRoot = path , loadCache = cache
src/Cryptol/REPL/Browse.hs view
@@ -6,8 +6,6 @@ import qualified Data.Map as Map import Data.Maybe(mapMaybe) import Data.List(sortBy)-import Data.Void (Void)-import qualified Prettyprinter as PP import Cryptol.Parser.AST(Pragma(..)) import qualified Cryptol.TypeCheck.Type as T@@ -38,7 +36,7 @@ ] disp = DispInfo { dispHow = how, env = mctxNameDisp mc }- decls = filterIfaceDecls (`Set.member` visNames) (mctxDecls mc)+ decls = filterIfaceDecls (`Set.member` visUserNames) (mctxDecls mc) allNames = namingEnvNames (mctxNames mc) notAnon nm = identIsNormal (nameIdent nm) && case nameModPathMaybe nm of@@ -48,6 +46,7 @@ case how of BrowseInScope -> allNames BrowseExported -> mctxExported mc+ visUserNames = Set.filter (\n -> nameSrc n == UserName) visNames data DispInfo = DispInfo { dispHow :: BrowseHow, env :: NameDisp }
src/Cryptol/REPL/Command.hs view
@@ -112,6 +112,7 @@ import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap import qualified Cryptol.Parser.AST as P+import Cryptol.Parser.Name (mkUnqual) import qualified Cryptol.Project as Proj import qualified Cryptol.Transform.Specialize as S import Cryptol.Symbolic@@ -1845,7 +1846,7 @@ } liftModuleCmd (M.evalDecls [T.NonRecursive decl]) denv <- getDynEnv- let nenv' = M.singletonNS M.NSValue (P.UnQual itIdent) freshIt+ let nenv' = M.singletonNS M.NSValue (mkUnqual itIdent) freshIt `M.shadowing` M.deNames denv setDynEnv $ denv { M.deNames = nenv' } return freshIt@@ -2285,7 +2286,7 @@ checkDocStringsCmd :: String {- ^ module name -} -> REPL CommandResult-checkDocStringsCmd input = withModule input (checkModName 0)+checkDocStringsCmd input = withModule input (fmap snd . checkModName Nothing 0) countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)@@ -2299,39 +2300,39 @@ | crSuccess (srResult result) = (successes + 1, nofences, failures) | otherwise = (successes, nofences, failures + 1) -withValidModule :: P.ModName -> String -> (M.LoadedModule -> REPL CommandResult) -> REPL CommandResult-withValidModule mn tab f =+withValidModule :: P.ModName -> String -> (CommandResult -> REPL a) -> (M.LoadedModule -> REPL a) -> REPL a+withValidModule mn tab kNo kYes = do env <- getModuleEnv case M.lookupModule mn env of Nothing -> case M.lookupSignature mn env of Nothing -> do rPutStrLn (tab ++ "Module " ++ show mn ++ " is not loaded")- pure emptyCommandResult { crSuccess = False }+ kNo emptyCommandResult { crSuccess = False } Just{} -> do rPutStrLn (tab ++ "Skipping docstrings on interface module")- pure emptyCommandResult+ kNo emptyCommandResult Just fe | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do rPutStrLn (tab ++ "Skipping docstrings on parameterized module")- pure emptyCommandResult- | otherwise -> f fe+ kNo emptyCommandResult+ | otherwise -> kYes fe -checkModName :: Int -> P.ModName -> REPL CommandResult-checkModName ind mn =- withValidModule mn tab (\m -> do- (results,_) <- checkDocStrings m Nothing+checkModName :: Maybe Proj.CacheId -> Int -> P.ModName -> REPL (Maybe Proj.CacheId, CommandResult)+checkModName mbCid ind mn =+ withValidModule mn tab (\r -> pure (mbCid,r)) (\m -> do+ (results,newCid) <- checkDocStrings m mbCid let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results] rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures)- pure emptyCommandResult { crSuccess = failures == 0 })+ pure (Just newCid, emptyCommandResult { crSuccess = failures == 0 })) where tab = replicate ind ' ' checkModNameForPrint :: P.ModName -> REPL CommandResult checkModNameForPrint mn =- withValidModule mn "" (\m -> do+ withValidModule mn "" pure (\m -> do printDocStrings m pure emptyCommandResult { crSuccess = True }) @@ -2352,48 +2353,12 @@ Right ((fps, mp, docstringResults),env) -> do setModuleEnv env let cache0 = fmap (\fp -> Proj.CacheEntry { cacheDocstringResult = Nothing, cacheFingerprint = fp }) fps- (cache, success) <-- foldM (\(fpAcc_, success_) (k, v) ->- case k of- M.InMem{} -> pure (fpAcc_, success_)- M.InFile path ->- case v of- Proj.Invalid e ->- do rPrint ("Failed to process module:" <+> (text path <> ":") $$- indent 2 (ppInvalidStatus e))- pure (fpAcc_, False) -- report failure- Proj.Scanned Proj.Unchanged _ ms ->- foldM f (fpAcc_, success_) ms- where- f (fpAcc, success) (m, _) =- do let name = P.thing (P.mName m)- case join (Map.lookup (Proj.CacheInFile path) docstringResults) of- Just True ->- do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"])- let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc- pure (fpAcc', success) -- preserve success-- Just False ->- do rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"])- let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc- pure (fpAcc', False) -- preserve failure-- Nothing ->- do checkRes <- checkModName 2 name- let success1 = crSuccess checkRes- let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just success1 }) (Proj.CacheInFile path) fpAcc- pure (fpAcc', success && success1)-- Proj.Scanned Proj.Changed _ ms ->- foldM f (fpAcc_, success_) ms- where- f (fpAcc, success) (m, _) =- do let name = P.thing (P.mName m)- checkRes <- checkModName 2 name- let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc- pure (fpAcc', success && crSuccess checkRes)+ (cache1, needCheck, success1) <-+ foldM (updateStatus docstringResults) (cache0, [], True) (Map.assocs mp)+ cacheId <- io (Proj.saveLoadCache (Proj.LoadCache cache1)) - ) (cache0, True) (Map.assocs mp)+ -- Revalidate modules, updating cache as you go+ (_cacheId, cache, success) <- foldM doCheck (Just cacheId, cache1, success1) (reverse needCheck) let (passing, failing, missing) = foldl@@ -2406,8 +2371,60 @@ rPutStrLn ("Passing: " ++ show passing ++ ", Failing: " ++ show failing ++ ", Missing: " ++ show missing) - _cacheId <- io (Proj.saveLoadCache (Proj.LoadCache cache)) pure emptyCommandResult { crSuccess = success }++ where+ doCheck (cid, fpAcc, success) (path, m) =+ do+ let name = P.thing (P.mName m)+ (newCid, checkRes) <- checkModName cid 2 name+ let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc+ pure (newCid, fpAcc', success && crSuccess checkRes)++ -- Check if some modules need to be revalidated.+ updateStatus curCache (fpAcc_, needCheck_, success_) (k, v) =+ case k of+ M.InMem{} -> pure (fpAcc_, needCheck_, success_)++ M.InFile path ->+ case v of+ Proj.Invalid e ->+ do rPrint ("Failed to process module:" <+> (text path <> ":") $$+ indent 2 (ppInvalidStatus e))+ pure (fpAcc_, needCheck_, False) -- report failure+ Proj.Scanned Proj.Unchanged _ ms -> foldM f (fpAcc_, needCheck_, success_) ms+ where+ f (fpAcc, needCheck, success) (m, _) =+ do let name = P.thing (P.mName m)+ case join (Map.lookup (Proj.CacheInFile path) curCache) of+ Just True ->+ do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"])+ let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc+ pure (fpAcc', needCheck, success) -- preserve success++ Just False ->+ case mode of+ Proj.UntestedMode Proj.RecheckFailed ->+ do+ let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc+ pure (fpAcc', (path, m) : needCheck, success)+ _ ->+ do + rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"])+ let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc+ pure (fpAcc', needCheck, False) -- preserve fail+ + Nothing -> pure (fpAcc', newNeedCheck, success)+ where+ fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc+ newNeedCheck =+ case mode of+ Proj.ModifiedMode -> needCheck+ _ -> (path, m) : needCheck+ + Proj.Scanned Proj.Changed _ ms -> pure (fpAcc', reverse pms ++ needCheck_, success_)+ where pms = [ (path, m) | (m, _) <- ms ]+ fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc_ -- | Get the path to the SAW command. -- Search options, in order:
src/Cryptol/REPL/Monad.hs view
@@ -104,8 +104,10 @@ import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Env as M import qualified Cryptol.ModuleSystem.Name as M+import qualified Cryptol.ModuleSystem.Names as M import qualified Cryptol.ModuleSystem.NamingEnv as M import Cryptol.Parser (ParseError,ppError)+import Cryptol.Parser.Name (NameSource(..)) import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError) import Cryptol.Parser.NoPat (Error) import Cryptol.Parser.Position (emptyRange, Range(from))@@ -136,7 +138,7 @@ import Data.IORef (IORef,newIORef,readIORef,atomicModifyIORef) import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)-import Data.Maybe (catMaybes)+import Data.Maybe (catMaybes, isJust) import Data.Ord (comparing) import Data.Tuple (swap) import Data.Typeable (Typeable)@@ -534,8 +536,6 @@ getLoadedMod :: REPL (Maybe LoadedModule) getLoadedMod = eLoadedMod `fmap` getRW -- -- | Set the path for the ':e' command. -- Note that this does not change the focused module (i.e., what ":r" reloads) setEditPath :: FilePath -> REPL ()@@ -659,14 +659,19 @@ getFocusedEnv = M.focusedEnv <$> getModuleEnv -- | Get visible variable names.--- This is used for command line completition.+-- This is used for command line completion. getExprNames :: REPL [String] getExprNames =- do fNames <- M.mctxNames <$> getFocusedEnv- return (map (show . pp) (Map.keys (M.namespaceMap M.NSValue fNames)))+ do + fNames <- M.mctxNames <$> getFocusedEnv+ let mnames = M.namespaceMap M.NSValue fNames+ let userNamesMap = + Map.filterWithKey (\_k v -> isJust (M.filterNames (\n -> UserName == M.nameSrc n) v)) mnames+ return (map (show . pp) (Map.keys userNamesMap)) + -- | Get visible type signature names.--- This is used for command line completition.+-- This is used for command line completion. getTypeNames :: REPL [String] getTypeNames = do fNames <- M.mctxNames <$> getFocusedEnv@@ -788,7 +793,7 @@ -- | Generate a fresh name using the given index. The name will reside within -- the "<interactive>" namespace.-freshName :: I.Ident -> M.NameSource -> REPL M.Name+freshName :: I.Ident -> NameSource -> REPL M.Name freshName i sys = M.liftSupply (M.mkDeclared I.NSValue mpath sys i Nothing emptyRange) where mpath = M.TopModule I.interactiveName
src/Cryptol/Transform/MonoValues.hs view
@@ -79,7 +79,7 @@ module Cryptol.Transform.MonoValues (rewModule) where import Cryptol.ModuleSystem.Name- (SupplyT,liftSupply,Supply,mkDeclared,NameSource(..),ModPath(..))+ (SupplyT,liftSupply,Supply,mkDeclared,ModPath(..), NameSource(..)) import Cryptol.Parser.Position (emptyRange) import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one import Cryptol.TypeCheck.TypeMap
src/Cryptol/TypeCheck/Default.hs view
@@ -22,10 +22,14 @@ -- | We default constraints of the form @Literal t a@ and @FLiteral m n r a@. -- -- For @Literal t a@ we examine the context of constraints on the type @a@--- to decide how to default. If @Logic a@ is required,--- we cannot do any defaulting. Otherwise, we default--- to either @Integer@ or @Rational@. In particular, if--- we need to satisfy the @Field a@, constraint, we choose+-- to decide how to default.+-- +-- We do NOT default if:+-- * `Logic t` and `a` in `fvs t`+-- * `Integral t`, and `t /= a`, and `a` in `fvs t`+--+-- Otherwise, we default to either @Integer@ or @Rational@.+-- In particular, if we need to satisfy the @Field a@, constraint, we choose -- @Rational@ and otherwise we choose @Integer@. -- -- For @FLiteral t a@ we always default to @Rational@.@@ -39,6 +43,20 @@ isLiteralGoal a = isJust (Map.lookup a (literalGoals gSet)) || isJust (Map.lookup a (literalLessThanGoals gSet))++ disableDefaultPred a p =+ case pIsLogic p of+ Just t -> a `Set.member` fvs t+ Nothing ->+ case pIsIntegral p of+ Just t ->+ case tIsVar t of+ Just _ -> False + Nothing -> a `Set.member` fvs t+ Nothing -> False++ disableDefault a = any (disableDefaultPred a) allProps+ tryDefVar a = -- If there is an `FLiteral` constraint we use that for defaulting. case Map.lookup a (flitDefaultCandidates gSet) of@@ -46,10 +64,10 @@ -- Otherwise we try to use a `Literal` Nothing- | isLiteralGoal a -> do- defT <- if has pLogic a then mzero- else if has pField a && not (has pIntegral a)- then pure tRational+ | isLiteralGoal a && not (disableDefault a) -> do+ defT <- + if has pField a && not (has pIntegral a)+ then pure tRational else if not (has pField a) then pure tInteger else mzero let d = tvInfo a
src/Cryptol/TypeCheck/Error.hs view
@@ -10,7 +10,7 @@ import qualified Data.Set as Set import Control.DeepSeq(NFData) import GHC.Generics(Generic)-import Data.List((\\),sortBy,partition)+import Data.List((\\),sortBy,partition,intersperse) import Data.Function(on) import Cryptol.Utils.Ident(Ident,Namespace(..))@@ -89,6 +89,7 @@ | DefaultingWildType P.Kind | DefaultingTo !TVarInfo Type | NonExhaustivePropGuards Name+ | DuplicateDeriving PC deriving (Show, Generic, NFData) -- | Various errors that might happen during type checking/inference@@ -117,6 +118,19 @@ -- More patterns provided for a bind than expected, -- given its signature. + | ClassNotDerivable+ -- ^ Deriving unsupported typeclass+ Name -- ^ The thing that the user tried to derive+ String -- ^ Description of the type declaration+ [PC] -- ^ The supported typeclasses for deriving on this+ -- sort of type declaration++ | DerivingMissingSuperclasses+ -- ^ Deriving instance for a class without deriving instances+ -- for its superclasses+ PC -- ^ The class listed in the deriving clause+ [PC] -- ^ Its superclasses not listed in the deriving clause+ | TypeMismatch TypeSource Path Type Type -- ^ Expected type, inferred type @@ -161,9 +175,9 @@ -- ^ Too many positional type arguments, in an explicit -- type instantiation - | BadParameterKind TParam Kind- -- ^ Kind other than `*` or `#` given to parameter of- -- type synonym, newtype, function signature, etc.+ | BadParameterKind TParam Kind [Kind]+ -- ^ We expected one of the kinds in the list, but got+ -- the given one instead. | CannotMixPositionalAndNamedTypeParams @@ -245,6 +259,8 @@ KindMismatch {} -> 10 TyVarWithParams {} -> 9 TooManyParams{} -> 9+ ClassNotDerivable{} -> 8+ DerivingMissingSuperclasses{} -> 8 TypeMismatch {} -> 8 EnumTypeMismatch {} -> 7 SchemaMismatch {} -> 7@@ -301,6 +317,7 @@ DefaultingWildType {} -> warn DefaultingTo d ty -> DefaultingTo d $! (apSubst su ty) NonExhaustivePropGuards {} -> warn+ DuplicateDeriving {} -> warn instance FVS Warning where fvs warn =@@ -309,6 +326,7 @@ DefaultingWildType {} -> Set.empty DefaultingTo _ ty -> fvs ty NonExhaustivePropGuards {} -> Set.empty+ DuplicateDeriving {} -> Set.empty instance TVars Error where apSubst su err =@@ -322,6 +340,8 @@ SchemaMismatch i t1 t2 -> SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2) TooManyParams b t i j -> TooManyParams b !$ (apSubst su t) .$ i .$ j+ ClassNotDerivable {} -> err+ DerivingMissingSuperclasses {} -> err TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2) EnumTypeMismatch t -> EnumTypeMismatch !$ apSubst su t InvalidConPat {} -> err@@ -375,6 +395,8 @@ RecursiveTypeDecls {} -> Set.empty SchemaMismatch _ t1 t2 -> fvs (t1,t2) TooManyParams _ t _ _ -> fvs t+ ClassNotDerivable {} -> Set.empty+ DerivingMissingSuperclasses {} -> Set.empty TypeMismatch _ _ t1 t2 -> fvs (t1,t2) EnumTypeMismatch t -> fvs t InvalidConPat {} -> Set.empty@@ -393,7 +415,7 @@ UndefinedTypeParameter {} -> Set.empty RepeatedTypeParameter {} -> Set.empty AmbiguousSize _ t -> fvs t- BadParameterKind tp _ -> Set.singleton (TVBound tp)+ BadParameterKind tp _ _ -> Set.singleton (TVBound tp) BareTypeApp -> Set.empty @@ -440,6 +462,9 @@ text "Could not prove that the constraint guards used in defining" <+> pp n <+> text "were exhaustive." + DuplicateDeriving pc ->+ "Duplicate" <+> pp pc <+> "in deriving clause"+ instance PP (WithNames Error) where ppPrec _ (WithNames err names) = case err of@@ -506,6 +531,16 @@ , "Actual number of parameters:" <+> int i , "When defining" <+> quotes ((pp n <> ":") <+> ppWithNames names t) ] + ClassNotDerivable badCls declDesc allowed ->+ "Cannot derive" <+> backticks (pp badCls) $$+ nested ("Derivable constraints for" <+> text declDesc <+> "declarations are:")+ (commaSepFill (map pp allowed))++ DerivingMissingSuperclasses pc supers ->+ "Missing superclass(es) for" <+> pp pc $$+ "To derive this constraint, you must also derive:" <+>+ commaSepFill (map pp supers)+ TypeMismatch src pa t1 t2 -> addTVarsDescsAfter names err $ nested "Type mismatch:" $@@ -600,10 +635,11 @@ ++ [ "When checking" <+> pp src ] ) - BadParameterKind tp k ->+ BadParameterKind tp k ks -> addTVarsDescsAfter names err $ vcat [ "Illegal kind assigned to type variable:" <+> ppWithNames names tp- , "Unexpected:" <+> pp k+ , "Expected:" <+> hsep (intersperse "or" (map pp ks))+ , "Actual:" <+> pp k ] TooManyPositionalTypeParams ->
src/Cryptol/TypeCheck/InferTypes.hs view
@@ -231,8 +231,24 @@ | CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive | CtFFI Name -- ^ Constraints on a foreign declaration required -- by the FFI (e.g. sequences must be finite)+ | CtDeriving -- ^ Required conditions for deriving+ Name -- ^ The type that the deriving clause is+ -- attached to+ PC -- ^ The class we are deriving+ DerivingConstraintSource -- ^ Which part of the type declaration caused+ -- this constraint deriving (Show, Generic, NFData) +-- | Where a condition for deriving arises from+data DerivingConstraintSource+ = NewtypeUnderlyingRecord -- ^ From the underlying record, when deriving for a+ -- newtype+ | EnumCtorField -- ^ From a constructor field of an enum+ Name -- ^ Name of the constructor+ Int -- ^ Index of the constructor field, starting from 0+ Type -- ^ Type of the constructor field+ deriving (Show, Generic, NFData)+ selSrc :: Selector -> TypeSource selSrc l = case l of RecordSel la _ -> TypeOfRecordField la@@ -249,7 +265,7 @@ CtComprehension -> src CtSplitPat -> src CtTypeSig -> src- CtInst e -> CtInst (apSubst su e)+ CtInst e -> CtInst $! apSubst su e CtSelector -> src CtExactType -> src CtEnumeration -> src@@ -260,8 +276,15 @@ CtModuleInstance _ -> src CtPropGuardsExhaustive _ -> src CtFFI _ -> src+ CtDeriving t p w -> CtDeriving t p $! apSubst su w +instance TVars DerivingConstraintSource where+ apSubst su src =+ case src of+ NewtypeUnderlyingRecord -> src+ EnumCtorField c i t -> EnumCtorField c i $! apSubst su t + instance FVS Goal where fvs g = fvs (goal g) @@ -371,6 +394,17 @@ CtModuleInstance r -> "module instantiation at" <+> pp r CtPropGuardsExhaustive n -> "exhaustion check for prop guards used in defining" <+> pp n CtFFI f -> "declaration of foreign function" <+> pp f+ CtDeriving t pc which -> pp which $$+ "when deriving instance" <+> parens (pp pc <+> pp t)++instance PP DerivingConstraintSource where+ ppPrec _ src =+ case src of+ NewtypeUnderlyingRecord -> "the underlying record of the newtype"+ EnumCtorField ctor i t ->+ -- Count starting from 1 when displaying to user+ "field" <+> int (i + 1) <+> "of constructor" <+> backticks (pp ctor) <+>+ parens ("type" <+> backticks (pp t)) ppUse :: Expr -> Doc ppUse expr =
src/Cryptol/TypeCheck/Kind.hs view
@@ -25,20 +25,27 @@ import qualified Cryptol.Parser.AST as P import Cryptol.Parser.Position+import Cryptol.ModuleSystem.Name(nameLoc) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Error-import Cryptol.TypeCheck.Subst(listSubst,apSubst)+import Cryptol.TypeCheck.Subst(listSubst,apSubst,isEmptySubst) import Cryptol.TypeCheck.Monad hiding (withTParams) import Cryptol.TypeCheck.SimpType(tRebuild) import Cryptol.TypeCheck.SimpleSolver(simplify)-import Cryptol.TypeCheck.Solve (simplifyAllConstraints)+import Cryptol.TypeCheck.Solve ( buildSolverCtxt+ , quickSolver+ , simplifyAllConstraints+ ) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP(pp,commaSep) import Cryptol.Utils.RecordMap +import Data.Map (Map) import qualified Data.Map as Map+import qualified Data.Set as Set+import Data.Foldable(foldlM) import Data.List(sortBy,groupBy)-import Data.Maybe(fromMaybe)+import Data.Maybe(fromMaybe,isJust) import Data.Function(on) import Data.Text (Text) import Control.Monad(unless,mplus,forM,when)@@ -91,15 +98,35 @@ --- | Check a module parameter declarations. Nothing much to check,--- we just translate from one syntax to another.+-- | Check a module parameter declaration.+-- We check that it has kind either * or #. checkParameterType :: P.ParameterType Name -> InferM ModTParam checkParameterType a =- do let mbDoc = P.ptDoc a- k = cvtK (P.ptKind a)- n = thing (P.ptName a)- return ModTParam { mtpKind = k, mtpName = n, mtpDoc = thing <$> mbDoc }-+ do+ let+ mbDoc = P.ptDoc a+ k = cvtK (P.ptKind a)+ n = thing (P.ptName a)+ mp = ModTParam { mtpKind = k, mtpName = n, mtpDoc = thing <$> mbDoc }+ case k of+ KNum -> pure mp+ KType -> pure mp+ _ ->+ do+ let mp' = mp { mtpKind = someKind k }+ inRange (nameLoc n)+ $ recordError (BadParameterKind (mtpParam mp') k [KNum,KType])+ pure mp'+ where+ -- When we find a malformed kind, we report an error, and correct the kind+ -- according to this function, as the rest of the code expects one of+ -- these kinds.+ someKind e =+ case e of+ _ :-> x -> someKind x+ KNum -> KNum+ KType -> KType+ KProp -> KType -- | Check a type-synonym declaration. checkTySyn :: P.TySyn Name -> Maybe Text -> InferM TySyn@@ -135,8 +162,8 @@ -- | Check a newtype declaration. checkNewtype :: P.Newtype Name -> Maybe Text -> InferM NominalType-checkNewtype (P.Newtype x as con fs) mbD =- do ((as1,fs1),gs) <- collectGoals $+checkNewtype (P.Newtype x as con fs derivs) mbDoc =+ do ((as1,fs1),bodyGs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams NoWildCards nominalParam as $ flip traverseRecordMap fs $ \_n (rng,f) ->@@ -144,17 +171,32 @@ simplifyAllConstraints return r + let name = thing x+ constraints = map goal bodyGs+ derivConds <-+ checkDeriving name newtypeDerivable derivs constraints+ [(TRec fs1, NewtypeUnderlyingRecord)]+ return NominalType { ntName = thing x , ntKind = KType , ntParams = as1- , ntConstraints = map goal gs+ , ntConstraints = constraints , ntDef = Struct StructCon { ntConName = con, ntFields = fs1 }+ , ntDeriving = derivConds , ntFixity = Nothing- , ntDoc = mbD+ , ntDoc = mbDoc } +-- | A description of newtype declarations, and the supported classes for+-- deriving on newtypes.+newtypeDerivable :: (String, [PC])+newtypeDerivable =+ ( "newtype"+ , [PEq, PCmp, PSignedCmp, PZero, PLogic, PRing]+ )+ checkEnum :: P.EnumDecl Name -> Maybe Text -> InferM NominalType checkEnum ed mbD = do let x = P.eName ed@@ -175,16 +217,121 @@ } simplifyAllConstraints pure r++ let name = thing x+ constraints = map goal gs+ derivConds <-+ checkDeriving name enumDerivable (P.eDeriving ed) constraints $+ concatMap+ (\con -> zipWith (\t i -> (t, EnumCtorField (ecName con) i t))+ (ecFields con)+ [0..])+ cons1+ pure NominalType { ntName = thing x , ntParams = as1 , ntKind = KType- , ntConstraints = map goal gs+ , ntConstraints = constraints , ntDef = Enum cons1+ , ntDeriving = derivConds , ntFixity = Nothing , ntDoc = mbD } +-- | A description of enum declarations, and the supported classes for deriving+-- on enums.+enumDerivable :: (String, [PC])+enumDerivable =+ ( "enum"+ , [PEq, PCmp, PSignedCmp]+ )++-- | Check a deriving clause, returning the derived classes and any conditions+-- that must be satisfied for the instances to hold.+checkDeriving ::+ Name+ -- ^ the type being declared+ -> (String, [PC])+ -- ^ description of the type being declared, and the allowed typeclasses+ -- for deriving on this sort of declaration+ -> [Located Name]+ -- ^ list of names in the @deriving@ clause+ -> [Prop]+ -- ^ constraints generated from the type declaration's body+ -> [(Type, DerivingConstraintSource)]+ -- ^ field types within the type declaration, and where they come from+ -> InferM (Map PC [Prop])+ -- ^ map from derived typeclasses to their conditions+checkDeriving declName (declDesc, allowed) derivs constraints fieldTypes = do+ -- Check that the names in the deriving clause are allowed and contain no+ -- duplicates.+ let addDerivRange derivRangeMap deriv = do+ let derivName = thing deriv+ derivRange = srcRange deriv+ case builtInType derivName of+ Just (PC pc)+ | pc `elem` allowed -> do+ let (existing, derivRangeMap') =+ Map.insertLookupWithKey (\_ _ old -> old)+ pc+ derivRange+ derivRangeMap+ when (isJust existing) $+ inRange derivRange $+ recordWarning $ DuplicateDeriving pc+ pure derivRangeMap'+ _ -> do+ recordErrorLoc (Just derivRange) $+ ClassNotDerivable derivName declDesc allowed+ pure derivRangeMap+ derivRangeMap <- foldlM addDerivRange mempty derivs+ -- We can use the functor constraints and the constraints generated from the+ -- body of the type declaration as assumptions for the solver.+ paramConstraints <- getParamConstraints+ let ctxt = buildSolverCtxt (constraints ++ map thing paramConstraints)+ -- For each derived class, generate its conditions.+ let generateConds pc derivRange = do+ -- Ensure superclasses are explicitly derived.+ let missingSuperclasses =+ Set.difference (typeSuperclassSet pc) (Map.keysSet derivRangeMap)+ unless (null missingSuperclasses) $+ recordErrorLoc (Just derivRange) $+ DerivingMissingSuperclasses pc (Set.toList missingSuperclasses)+ -- All fields in the type declaration must be instances of each class.+ let goals =+ map (\(ty, which) ->+ Goal { goal = TCon (PC pc) [ty]+ , goalSource = CtDeriving declName pc which+ , goalRange = derivRange+ })+ fieldTypes+ case quickSolver ctxt goals of+ Right (su, conds)+ -- Since we are not doing type inference, su should be empty.+ | isEmptySubst su ->+ -- conds contains the goals that the solver was unable to solve,+ -- but unable to rule out either (e.g. goals involving a type+ -- parameter, which can only be solved when this nominal type is+ -- actually used). These are the conditions that we want to save+ -- in the 'NominalType', so they can be checked at the use site of+ -- the class methods.+ pure $ Just $ map goal conds+ | otherwise ->+ panic "checkDeriving"+ [ "Solver substitution not empty"+ , "ctxt: " ++ show ctxt+ , "goals: " ++ show goals+ , "su: " ++ show su+ , "conds: " ++ show conds+ ]+ Left err -> do+ -- If there were unsolvable (impossible) goals, that means some+ -- fields were not instances of this class. Report the error here.+ recordErrorLoc (Just derivRange) err+ pure Nothing+ Map.traverseMaybeWithKey generateConds derivRangeMap+ checkPrimType :: P.PrimType Name -> Maybe Text -> InferM NominalType checkPrimType p mbD = do let (as,cs) = P.primTCts p@@ -205,6 +352,7 @@ , ntConstraints = cs' , ntDoc = mbD , ntDef = Abstract+ , ntDeriving = mempty } where splitK k =
src/Cryptol/TypeCheck/ModuleInstance.hs view
@@ -111,6 +111,7 @@ , ntKind = ntKind nt , ntConstraints = moduleInstance (ntConstraints nt) , ntDef = moduleInstance (ntDef nt)+ , ntDeriving = moduleInstance <$> ntDeriving nt , ntFixity = ntFixity nt , ntDoc = ntDoc nt }
src/Cryptol/TypeCheck/Monad.hs view
@@ -39,7 +39,7 @@ import Cryptol.ModuleSystem.Name (FreshM(..),Supply,mkLocal,asLocal- , nameInfo, NameInfo(..),NameSource(..), nameTopModule)+ , nameInfo, NameInfo(..),NameSource(..),nameTopModule) import Cryptol.ModuleSystem.NamingEnv.Types import qualified Cryptol.ModuleSystem.Interface as If import Cryptol.Parser.Position@@ -633,13 +633,13 @@ KNum -> return () KType -> return () KProp -> return ()- _ -> recordError (BadParameterKind tp k)+ _ -> recordError (BadParameterKind tp k [KNum, KType, KProp]) starOrHash = case k of KNum -> return () KType -> return ()- _ -> recordError (BadParameterKind tp k)+ _ -> recordError (BadParameterKind tp k [KNum,KType]) -- | Generate a new free type variable. newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
src/Cryptol/TypeCheck/SimpleSolver.hs view
@@ -7,7 +7,8 @@ import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType) import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq, cryIsPrime) import Cryptol.TypeCheck.Solver.Class- ( solveZeroInst, solveLogicInst, solveRingInst+ ( solveDerivedInst+ , solveZeroInst, solveLogicInst, solveRingInst , solveIntegralInst, solveFieldInst, solveRoundInst , solveEqInst, solveCmpInst, solveSignedCmpInst , solveLiteralInst@@ -46,6 +47,9 @@ case tNoUser prop of TCon (PC PTrue) [] -> SolvedIf [] TCon (PC PAnd) [l,r] -> SolvedIf [l,r]++ TCon (PC pc) [ty]+ | TNominal nt targs <- tNoUser ty -> solveDerivedInst pc nt targs TCon (PC PZero) [ty] -> solveZeroInst ty TCon (PC PLogic) [ty] -> solveLogicInst ty
src/Cryptol/TypeCheck/Solve.hs view
@@ -14,6 +14,8 @@ , proveModuleTopLevel , defaultAndSimplify , defaultReplExpr+ , quickSolver+ , buildSolverCtxt ) where import Cryptol.Parser.Position(thing,emptyRange)
src/Cryptol/TypeCheck/Solver/Class.hs view
@@ -11,7 +11,11 @@ {-# LANGUAGE PatternGuards #-} module Cryptol.TypeCheck.Solver.Class- ( solveZeroInst+ ( solveDerivedInst+ -- * Built-in instances+ --+ -- $builtInInstances+ , solveZeroInst , solveLogicInst , solveRingInst , solveFieldInst@@ -26,11 +30,13 @@ , solveValidFloat ) where +import qualified Data.Map as Map import qualified LibBF as FP import Cryptol.TypeCheck.Type hiding (tSub) import Cryptol.TypeCheck.SimpType (tAdd,tSub,tWidth,tMax) import Cryptol.TypeCheck.Solver.Types+import Cryptol.TypeCheck.Subst.Type (listParamSubst, apSubstNoSimp) import Cryptol.Utils.RecordMap {- | This places constraints on the floating point numbers that@@ -65,6 +71,25 @@ +-- | Solve a constraint on a nominal type by looking up its derived instance.+solveDerivedInst :: PC -- ^ the typeclass (of kind @* -> Prop@)+ -> NominalType -- ^ the type constructor+ -> [Type] -- ^ type arguments to the 'NominalType'+ -> Solved+solveDerivedInst pc nt targs =+ case Map.lookup pc (ntDeriving nt) of+ Just conds ->+ -- The conditions saved in the type may refer to the type parameters, so+ -- we need to instantiate them with the type arguments.+ let subst = listParamSubst $ zip (ntParams nt) targs+ in SolvedIf $ map (apSubstNoSimp subst) conds+ Nothing -> Unsolvable++-- $builtInInstances+-- The functions below only solve for built-in instances. To solve for derived+-- instances, check first if the type is 'TNominal' and use 'solveDerivedInst'+-- in that case.+ -- | Solve a Zero constraint by instance, if possible. solveZeroInst :: Type -> Solved solveZeroInst ty = case tNoUser ty of@@ -101,9 +126,6 @@ -- (Zero a, Zero b) => Zero { x1 : a, x2 : b } TRec fs -> SolvedIf [ pZero ety | ety <- recordElements fs ] - -- Zero <nominal> -> fails- TNominal {} -> Unsolvable- _ -> Unsolved -- | Solve a Logic constraint by instance, if possible.@@ -140,9 +162,6 @@ -- (Logic a, Logic b) => Logic { x1 : a, x2 : b } TRec fs -> SolvedIf [ pLogic ety | ety <- recordElements fs ] - -- Logic <nominal> -> fails- TNominal {} -> Unsolvable- _ -> Unsolved @@ -180,9 +199,6 @@ -- (Ring a, Ring b) => Ring { x1 : a, x2 : b } TRec fs -> SolvedIf [ pRing ety | ety <- recordElements fs ] - -- Ring <nominal> -> fails- TNominal {} -> Unsolvable- _ -> Unsolved @@ -350,9 +366,6 @@ -- (Eq a, Eq b) => Eq { x:a, y:b } TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ] - -- Eq <nominal> -> fails- TNominal {} -> Unsolvable- _ -> Unsolved @@ -390,9 +403,6 @@ -- (Cmp a, Cmp b) => Cmp { x:a, y:b } TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ] - -- Cmp <nominal> -> fails- TNominal{} -> Unsolvable- _ -> Unsolved @@ -444,9 +454,6 @@ -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b } TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ]-- -- SignedCmp <nominal> -> fails- TNominal{} -> Unsolvable _ -> Unsolved
src/Cryptol/TypeCheck/Solver/Improve.hs view
@@ -20,7 +20,7 @@ -- | Improvements from a bunch of propositions. -- Invariant:--- the substitions should be already applied to the new sub-goals, if any.+-- the substitutions should be already applied to the new sub-goals, if any. improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst,[Prop]) improveProps impSkol ctxt ps0 = loop emptySubst ps0 where@@ -40,13 +40,25 @@ -- | Improvements from a proposition. -- Invariant:--- the substitions should be already applied to the new sub-goals, if any.+-- the substitutions should be already applied to the new sub-goals, if any. improveProp :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop]) improveProp impSkol ctxt prop = improveEq impSkol ctxt prop <|>- improveLit impSkol prop+ improveLit impSkol prop <|>+ improveIntegral impSkol prop -- XXX: others +-- Whenever we have `Integral [m]a`, we can learn that `a = Bit`+improveIntegral :: Bool -> Prop -> Match (Subst,[Prop])+improveIntegral impSkol prop =+ do+ t <- aIntegral prop+ (_,b) <- aSeq t+ a <- aTVar b+ unless impSkol $ guard (isFreeTV a)+ let su = uncheckedSingleSubst a tBit+ return (su, [])+ -- Whenever we have `Literal n [m]a`, -- we can learn that `a = Bit` improveLit :: Bool -> Prop -> Match (Subst, [Prop])@@ -61,7 +73,7 @@ -- | Improvements from equality constraints. -- Invariant:--- the substitions should be already applied to the new sub-goals, if any.+-- the substitutions should be already applied to the new sub-goals, if any. improveEq :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop]) improveEq impSkol fins prop = do (lhs,rhs) <- (|=|) prop
src/Cryptol/TypeCheck/Solver/Types.hs view
@@ -13,7 +13,7 @@ SolverCtxt { intervals :: Map TVar Interval , saturatedAsmps :: Set Prop- }+ } deriving Show instance Semigroup Ctxt where SolverCtxt is1 as1 <> SolverCtxt is2 as2 = SolverCtxt (is1 <> is2) (as1 <> as2)
src/Cryptol/TypeCheck/Subst.hs view
@@ -9,8 +9,6 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Safe #-} module Cryptol.TypeCheck.Subst ( Subst@@ -39,109 +37,12 @@ import Data.Either (partitionEithers) import qualified Data.Map.Strict as Map import qualified Data.IntMap as IntMap-import Data.Set (Set)-import qualified Data.Set as Set import Cryptol.TypeCheck.AST-import Cryptol.TypeCheck.PP+import Cryptol.TypeCheck.Subst.Type import Cryptol.TypeCheck.TypeMap-import qualified Cryptol.TypeCheck.SimpType as Simp import qualified Cryptol.TypeCheck.SimpleSolver as Simp-import Cryptol.Utils.Panic(panic)-import Cryptol.Utils.Misc (anyJust, anyJust2) --- | A 'Subst' value represents a substitution that maps each 'TVar'--- to a 'Type'.------ Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a--- type @t@, then @t@ must not mention (directly or indirectly) any--- type parameter that is not in @tps@. In particular, if @t@ contains--- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of--- @tps@. This ensures that applying the substitution will not permit--- any type parameter to escape from its scope.------ Invariant 2: The substitution must be idempotent, in that applying--- a substitution to any 'Type' in the map should leave that 'Type'--- unchanged. In other words, 'Type' values in the range of a 'Subst'--- should not mention any 'TVar' in the domain of the 'Subst'. In--- particular, this implies that a substitution must not contain any--- recursive variable mappings.------ Invariant 3: The substitution must be kind correct: Each 'TVar' in--- the substitution must map to a 'Type' of the same kind.--data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))- , suBoundMap :: !(IntMap.IntMap (TVar, Type))- , suDefaulting :: !Bool- }- deriving Show--emptySubst :: Subst-emptySubst =- S { suFreeMap = IntMap.empty- , suBoundMap = IntMap.empty- , suDefaulting = False- }--mergeDistinctSubst :: [Subst] -> Subst-mergeDistinctSubst sus =- case sus of- [] -> emptySubst- _ -> foldr1 merge sus-- where- merge s1 s2 = S { suFreeMap = jn suFreeMap s1 s2- , suBoundMap = jn suBoundMap s1 s2- , suDefaulting = if suDefaulting s1 || suDefaulting s2- then err- else False- }-- err = panic "mergeDistinctSubst" [ "Not distinct" ]- bad _ _ = err- jn f x y = IntMap.unionWith bad (f x) (f y)--------- | Reasons to reject a single-variable substitution.-data SubstError- = SubstRecursive- -- ^ 'TVar' maps to a type containing the same variable.- | SubstEscaped [TParam]- -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.- | SubstKindMismatch Kind Kind- -- ^ 'TVar' maps to a type with a different kind.--singleSubst :: TVar -> Type -> Either SubstError Subst-singleSubst x t- | kindOf x /= kindOf t = Left (SubstKindMismatch (kindOf x) (kindOf t))- | x `Set.member` fvs t = Left SubstRecursive- | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))- | otherwise = Right (uncheckedSingleSubst x t)- where- escaped =- case x of- TVBound _ -> Set.empty- TVFree _ _ scope _ -> freeParams t `Set.difference` scope--uncheckedSingleSubst :: TVar -> Type -> Subst-uncheckedSingleSubst v@(TVFree i _ _tps _) t =- S { suFreeMap = IntMap.singleton i (v, t)- , suBoundMap = IntMap.empty- , suDefaulting = False- }-uncheckedSingleSubst v@(TVBound tp) t =- S { suFreeMap = IntMap.empty- , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)- , suDefaulting = False- }--singleTParamSubst :: TParam -> Type -> Subst-singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t- (@@) :: Subst -> Subst -> Subst s2 @@ s1 | isEmptySubst s2 =@@ -156,72 +57,8 @@ , suDefaulting = suDefaulting s1 || suDefaulting s2 } --- | A defaulting substitution maps all otherwise-unmapped free--- variables to a kind-appropriate default type (@Bit@ for value types--- and @0@ for numeric types).-defaultingSubst :: Subst -> Subst-defaultingSubst s = s { suDefaulting = True } --- | Makes a substitution out of a list.--- WARNING: We do not validate the list in any way, so the caller should--- ensure that we end up with a valid (e.g., idempotent) substitution.-listSubst :: [(TVar, Type)] -> Subst-listSubst xs- | null xs = emptySubst- | otherwise = S { suFreeMap = IntMap.fromList frees- , suBoundMap = IntMap.fromList bounds- , suDefaulting = False }- where- (frees, bounds) = partitionEithers (map classify xs)- classify x =- case fst x of- TVFree i _ _ _ -> Left (i, x)- TVBound tp -> Right (tpUnique tp, x) --- | Makes a substitution out of a list.--- WARNING: We do not validate the list in any way, so the caller should--- ensure that we end up with a valid (e.g., idempotent) substitution.-listParamSubst :: [(TParam, Type)] -> Subst-listParamSubst xs- | null xs = emptySubst- | otherwise = S { suFreeMap = IntMap.empty- , suBoundMap = IntMap.fromList bounds- , suDefaulting = False }- where- bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ]--isEmptySubst :: Subst -> Bool-isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su)---- Returns the empty set if this is a defaulting substitution-substBinds :: Subst -> Set TVar-substBinds su- | suDefaulting su = Set.empty- | otherwise = Set.fromList (map fst (assocsSubst su))--substToList :: Subst -> [(TVar, Type)]-substToList s- | suDefaulting s = panic "substToList" ["Defaulting substitution."]- | otherwise = assocsSubst s--assocsSubst :: Subst -> [(TVar, Type)]-assocsSubst s = frees ++ bounds- where- frees = IntMap.elems (suFreeMap s)- bounds = IntMap.elems (suBoundMap s)--instance PP (WithNames Subst) where- ppPrec _ (WithNames s mp)- | null els = text "(empty substitution)"- | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els))- where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t- els = assocsSubst s--instance PP Subst where- ppPrec n = ppWithNamesPrec IntMap.empty n--- infixl 0 !$ infixl 0 .$ @@ -247,69 +84,12 @@ where f' x = Done $! f x -- | Apply a substitution. Returns `Nothing` if nothing changed.+-- Performs simplification on the result. apSubstMaybe :: Subst -> Type -> Maybe Type-apSubstMaybe su ty =- case ty of- TCon t ts ->- do ss <- anyJust (apSubstMaybe su) ts- case t of- TF _ -> Just $! Simp.tCon t ss- PC _ -> Just $! Simp.simplify mempty (TCon t ss)- _ -> Just (TCon t ss)-- TUser f ts t ->- do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe su)) (apSubstMaybe su) (ts, t)- Just (TUser f ts1 t1)-- TRec fs -> TRec `fmap` (anyJust (apSubstMaybe su) fs)-- {- We apply the substitution to nominal types as well, because it might- contain module parameters, which need to be substituted when- instantiating a functor. -}- TNominal nt ts ->- uncurry TNominal <$> anyJust2 (applySubstToNominalType su)- (anyJust (apSubstMaybe su))- (nt,ts)-- TVar x -> applySubstToVar su x--lookupSubst :: TVar -> Subst -> Maybe Type-lookupSubst x su =- fmap snd $- case x of- TVFree i _ _ _ -> IntMap.lookup i (suFreeMap su)- TVBound tp -> IntMap.lookup (tpUnique tp) (suBoundMap su)+apSubstMaybe = apSubstMaybe' (Simp.simplify mempty) applySubstToVar :: Subst -> TVar -> Maybe Type-applySubstToVar su x =- case lookupSubst x su of- -- For a defaulting substitution, we must recurse in order to- -- replace unmapped free vars with default types.- Just t- | suDefaulting su -> Just $! apSubst su t- | otherwise -> Just t- Nothing- | suDefaulting su -> Just $! defaultFreeVar x- | otherwise -> Nothing---applySubstToNominalType :: Subst -> NominalType -> Maybe NominalType-applySubstToNominalType su nt =- do (cs,def) <- anyJust2 (anyJust (apSubstMaybe su)) apSubstDef- (ntConstraints nt, ntDef nt)- pure nt { ntConstraints = cs, ntDef = def }- where- apSubstDef d =- case d of- Struct c ->- do fs <- anyJust (apSubstMaybe su) (ntFields c)- pure (Struct c { ntFields = fs })- Enum cs -> Enum <$> anyJust apSubstCon cs- Abstract -> pure Abstract-- apSubstCon c =- do fs <- anyJust (apSubstMaybe su) (ecFields c)- pure c { ecFields = fs }+applySubstToVar = applySubstToVar' apSubstMaybe @@ -333,18 +113,6 @@ instance TVars Type where apSubst su ty = fromMaybe ty (apSubstMaybe su ty)---- | Pick types for unconstrained unification variables.-defaultFreeVar :: TVar -> Type-defaultFreeVar x@(TVBound {}) = TVar x-defaultFreeVar (TVFree _ k _ d) =- case k of- KType -> tBit- KNum -> tNum (0 :: Int)- _ -> panic "Cryptol.TypeCheck.Subst.defaultFreeVar"- [ "Free variable of unexpected kind."- , "Source: " ++ show d- , "Kind: " ++ show (pp k) ] instance (Traversable m, TVars a) => TVars (List m a) where apSubst su = fmap' (apSubst su)
+ src/Cryptol/TypeCheck/Subst/Type.hs view
@@ -0,0 +1,293 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}++-- | Most of this module is re-exported by "Cryptol.TypeCheck.Subst", so you+-- probably want to import that instead of this.+--+-- The exception being, if you want to substitute types without performing+-- simplification afterwards, then you should use 'apSubstNoSimp' from this+-- module. It is in this module so that you can use it from places like the+-- typeclass solver itself, to avoid a module import cycle (since the regular+-- 'Cryptol.TypeCheck.Subst.apSubst' has to import the class solver to do the+-- substitution).+module Cryptol.TypeCheck.Subst.Type+ ( Subst(..)+ , emptySubst+ , SubstError(..)+ , singleSubst+ , singleTParamSubst+ , uncheckedSingleSubst+ , defaultingSubst+ , listSubst+ , listParamSubst+ , isEmptySubst+ , substBinds+ , substToList+ , mergeDistinctSubst+ , apSubstMaybe'+ , applySubstToVar'+ , apSubstNoSimp+ ) where++import Data.Maybe+import Data.Either (partitionEithers)+import qualified Data.IntMap as IntMap+import Data.Set (Set)+import qualified Data.Set as Set++import Cryptol.TypeCheck.AST+import Cryptol.TypeCheck.PP+import qualified Cryptol.TypeCheck.SimpType as Simp+import Cryptol.Utils.Panic (panic)+import Cryptol.Utils.Misc (anyJust, anyJust2, anyJust3)++-- | A 'Subst' value represents a substitution that maps each 'TVar'+-- to a 'Type'.+--+-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a+-- type @t@, then @t@ must not mention (directly or indirectly) any+-- type parameter that is not in @tps@. In particular, if @t@ contains+-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of+-- @tps@. This ensures that applying the substitution will not permit+-- any type parameter to escape from its scope.+--+-- Invariant 2: The substitution must be idempotent, in that applying+-- a substitution to any 'Type' in the map should leave that 'Type'+-- unchanged. In other words, 'Type' values in the range of a 'Subst'+-- should not mention any 'TVar' in the domain of the 'Subst'. In+-- particular, this implies that a substitution must not contain any+-- recursive variable mappings.+--+-- Invariant 3: The substitution must be kind correct: Each 'TVar' in+-- the substitution must map to a 'Type' of the same kind.++data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))+ , suBoundMap :: !(IntMap.IntMap (TVar, Type))+ , suDefaulting :: !Bool+ }+ deriving Show++emptySubst :: Subst+emptySubst =+ S { suFreeMap = IntMap.empty+ , suBoundMap = IntMap.empty+ , suDefaulting = False+ }++mergeDistinctSubst :: [Subst] -> Subst+mergeDistinctSubst sus =+ case sus of+ [] -> emptySubst+ _ -> foldr1 merge sus++ where+ merge s1 s2 = S { suFreeMap = jn suFreeMap s1 s2+ , suBoundMap = jn suBoundMap s1 s2+ , suDefaulting = if suDefaulting s1 || suDefaulting s2+ then err+ else False+ }++ err = panic "mergeDistinctSubst" [ "Not distinct" ]+ bad _ _ = err+ jn f x y = IntMap.unionWith bad (f x) (f y)+++++++-- | Reasons to reject a single-variable substitution.+data SubstError+ = SubstRecursive+ -- ^ 'TVar' maps to a type containing the same variable.+ | SubstEscaped [TParam]+ -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.+ | SubstKindMismatch Kind Kind+ -- ^ 'TVar' maps to a type with a different kind.++singleSubst :: TVar -> Type -> Either SubstError Subst+singleSubst x t+ | kindOf x /= kindOf t = Left (SubstKindMismatch (kindOf x) (kindOf t))+ | x `Set.member` fvs t = Left SubstRecursive+ | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))+ | otherwise = Right (uncheckedSingleSubst x t)+ where+ escaped =+ case x of+ TVBound _ -> Set.empty+ TVFree _ _ scope _ -> freeParams t `Set.difference` scope++uncheckedSingleSubst :: TVar -> Type -> Subst+uncheckedSingleSubst v@(TVFree i _ _tps _) t =+ S { suFreeMap = IntMap.singleton i (v, t)+ , suBoundMap = IntMap.empty+ , suDefaulting = False+ }+uncheckedSingleSubst v@(TVBound tp) t =+ S { suFreeMap = IntMap.empty+ , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)+ , suDefaulting = False+ }++singleTParamSubst :: TParam -> Type -> Subst+singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t++-- | A defaulting substitution maps all otherwise-unmapped free+-- variables to a kind-appropriate default type (@Bit@ for value types+-- and @0@ for numeric types).+defaultingSubst :: Subst -> Subst+defaultingSubst s = s { suDefaulting = True }++-- | Makes a substitution out of a list.+-- WARNING: We do not validate the list in any way, so the caller should+-- ensure that we end up with a valid (e.g., idempotent) substitution.+listSubst :: [(TVar, Type)] -> Subst+listSubst xs+ | null xs = emptySubst+ | otherwise = S { suFreeMap = IntMap.fromList frees+ , suBoundMap = IntMap.fromList bounds+ , suDefaulting = False }+ where+ (frees, bounds) = partitionEithers (map classify xs)+ classify x =+ case fst x of+ TVFree i _ _ _ -> Left (i, x)+ TVBound tp -> Right (tpUnique tp, x)++-- | Makes a substitution out of a list.+-- WARNING: We do not validate the list in any way, so the caller should+-- ensure that we end up with a valid (e.g., idempotent) substitution.+listParamSubst :: [(TParam, Type)] -> Subst+listParamSubst xs+ | null xs = emptySubst+ | otherwise = S { suFreeMap = IntMap.empty+ , suBoundMap = IntMap.fromList bounds+ , suDefaulting = False }+ where+ bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ]++isEmptySubst :: Subst -> Bool+isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su)++-- Returns the empty set if this is a defaulting substitution+substBinds :: Subst -> Set TVar+substBinds su+ | suDefaulting su = Set.empty+ | otherwise = Set.fromList (map fst (assocsSubst su))++substToList :: Subst -> [(TVar, Type)]+substToList s+ | suDefaulting s = panic "substToList" ["Defaulting substitution."]+ | otherwise = assocsSubst s++assocsSubst :: Subst -> [(TVar, Type)]+assocsSubst s = frees ++ bounds+ where+ frees = IntMap.elems (suFreeMap s)+ bounds = IntMap.elems (suBoundMap s)++instance PP (WithNames Subst) where+ ppPrec _ (WithNames s mp)+ | null els = text "(empty substitution)"+ | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els))+ where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t+ els = assocsSubst s++instance PP Subst where+ ppPrec n = ppWithNamesPrec IntMap.empty n++-- | Apply a substitution. Returns `Nothing` if nothing changed.+-- The @Prop -> Prop@ function is how to simplify the result if it is a+-- predicate.+apSubstMaybe' :: (Prop -> Prop) -> Subst -> Type -> Maybe Type+apSubstMaybe' simpProp su ty =+ case ty of+ TCon t ts ->+ do ss <- anyJust (apSubstMaybe' simpProp su) ts+ case t of+ TF _ -> Just $! Simp.tCon t ss+ PC _ -> Just $! simpProp (TCon t ss)+ _ -> Just (TCon t ss)++ TUser f ts t ->+ do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe' simpProp su))+ (apSubstMaybe' simpProp su)+ (ts, t)+ Just (TUser f ts1 t1)++ TRec fs -> TRec `fmap` (anyJust (apSubstMaybe' simpProp su) fs)++ {- We apply the substitution to nominal types as well, because it might+ contain module parameters, which need to be substituted when+ instantiating a functor. -}+ TNominal nt ts ->+ uncurry TNominal <$> anyJust2 (applySubstToNominalType' simpProp su)+ (anyJust (apSubstMaybe' simpProp su))+ (nt,ts)++ TVar x -> applySubstToVar' (apSubstMaybe' simpProp) su x++-- | Apply a substitution without simplifying the result when it is a predicate.+--+-- This is used by the typeclass solver itself, if it needs to perform+-- substitution; e.g., when solving derived instances for nominal types. Some+-- code asks the typeclass solver to do only a single simplification step; if it+-- called the regular 'Cryptol.TypeCheck.Subst.apSubst' which simplifies+-- recursively after substitution, then it would do many simplification steps+-- instead of one, resulting in worse error messages. Not doing simplification+-- also allows us to avoid a module dependency cycle.+apSubstNoSimp :: Subst -> Type -> Type+apSubstNoSimp su ty = fromMaybe ty (apSubstMaybe' id su ty)++lookupSubst :: TVar -> Subst -> Maybe Type+lookupSubst x su =+ fmap snd $+ case x of+ TVFree i _ _ _ -> IntMap.lookup i (suFreeMap su)+ TVBound tp -> IntMap.lookup (tpUnique tp) (suBoundMap su)++applySubstToVar' :: (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type+applySubstToVar' substType su x =+ case lookupSubst x su of+ -- For a defaulting substitution, we must recurse in order to+ -- replace unmapped free vars with default types.+ Just t+ | suDefaulting su -> Just $! fromMaybe t (substType su t)+ | otherwise -> Just t+ Nothing+ | suDefaulting su -> Just $! defaultFreeVar x+ | otherwise -> Nothing++applySubstToNominalType' :: (Prop -> Prop)+ -> Subst -> NominalType -> Maybe NominalType+applySubstToNominalType' simpProp su nt =+ do (cs,def,der) <- anyJust3 (anyJust (apSubstMaybe' simpProp su))+ apSubstDef+ (anyJust (anyJust (apSubstMaybe' simpProp su)))+ (ntConstraints nt, ntDef nt, ntDeriving nt)+ pure nt { ntConstraints = cs, ntDef = def, ntDeriving = der }+ where+ apSubstDef d =+ case d of+ Struct c ->+ do fs <- anyJust (apSubstMaybe' simpProp su) (ntFields c)+ pure (Struct c { ntFields = fs })+ Enum cs -> Enum <$> anyJust apSubstCon cs+ Abstract -> pure Abstract++ apSubstCon c =+ do fs <- anyJust (apSubstMaybe' simpProp su) (ecFields c)+ pure c { ecFields = fs }++-- | Pick types for unconstrained unification variables.+defaultFreeVar :: TVar -> Type+defaultFreeVar x@(TVBound {}) = TVar x+defaultFreeVar (TVFree _ k _ d) =+ case k of+ KType -> tBit+ KNum -> tNum (0 :: Int)+ _ -> panic "Cryptol.TypeCheck.Subst.defaultFreeVar"+ [ "Free variable of unexpected kind."+ , "Source: " ++ show d+ , "Kind: " ++ show (pp k) ]
src/Cryptol/TypeCheck/Type.hs view
@@ -327,6 +327,13 @@ , ntKind :: !Kind -- ^ Result kind , ntConstraints :: [Prop] , ntDef :: NominalTypeDef+ , ntDeriving :: Map PC [Prop]+ -- ^ Derived classes and their conditions (which may contain type+ -- variables).+ --+ -- For instance, if we have @enum Maybe a = Nothing | Just a deriving (Eq)@,+ -- this map would be @{Eq -> [Eq a]}@, since the derived instance is+ -- @instance (Eq a) => Eq (Maybe a)@. , ntFixity :: !(Maybe Fixity) , ntDoc :: Maybe Text } deriving (Show, Generic, NFData)@@ -456,9 +463,17 @@ superclassSet (TCon (PC PPrime) [n]) = Set.fromList [ pFin n, n >== tTwo ] -superclassSet (TCon (PC p0) [t]) = go p0+superclassSet (TCon (PC p0) [t]) =+ Set.map (\p -> TCon (PC p) [t]) (typeSuperclassSet p0)++superclassSet _ = mempty++-- | Given a typeclass of kind @* -> Prop@, compute the set of all transitive+-- superclasses of kind @* -> Prop@.+typeSuperclassSet :: PC -> Set PC+typeSuperclassSet = go where- super p = Set.insert (TCon (PC p) [t]) (go p)+ super p = Set.insert p (go p) go PRing = super PZero go PLogic = super PZero@@ -468,8 +483,6 @@ go PCmp = super PEq go PSignedCmp = super PEq go _ = mempty--superclassSet _ = mempty nominalTypeConTypes :: NominalType -> [(Name,Schema)]
src/Cryptol/TypeCheck/TypePat.hs view
@@ -13,6 +13,7 @@ , aLiteral , aLiteralLessThan , aLogic+ , aIntegral , aTVar , aFreeTVar@@ -191,6 +192,9 @@ aLogic :: Pat Prop Type aLogic = tp PLogic ar1++aIntegral :: Pat Prop Type+aIntegral = tp PIntegral ar1 -------------------------------------------------------------------------------- anError :: Kind -> Pat Type ()
src/Cryptol/Utils/Misc.hs view
@@ -34,3 +34,11 @@ (Just x , Nothing) -> Just (x, b) (Nothing, Just y ) -> Just (a, y) (Just x , Just y ) -> Just (x, y)++-- | Apply functions to all 3 elements of a triple.+-- Returns 'Nothing' if nothing changed, and @Just triple@ otherwise.+anyJust3 :: (a -> Maybe a) -> (b -> Maybe b) -> (c -> Maybe c)+ -> (a, b, c) -> Maybe (a, b, c)+anyJust3 f g h (a, b, c) = do+ (a', (b', c')) <- anyJust2 f (anyJust2 g h) (a, (b, c))+ pure (a', b', c')