-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Cryptol: The Language of Cryptography -- -- 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/. @package cryptol @version 2.6.0 -- | Architecture-specific parts of the concrete evaluator go here. module Cryptol.Eval.Arch -- | This is the widest word we can have before gmp will fail to allocate -- and bring down the whole program. According to -- https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html -- the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however -- experiments show that it's somewhere under 2^37 at least on 64-bit Mac -- OS X. maxBigIntWidth :: Integer module Cryptol.Utils.Ident -- | Module names are just text. data ModName modNameToText :: ModName -> Text textToModName :: Text -> ModName modNameChunks :: ModName -> [String] packModName :: [Text] -> ModName preludeName :: ModName interactiveName :: ModName noModuleName :: ModName exprModName :: ModName isParamInstModName :: ModName -> Bool -- | Convert a parameterized module's name to the name of the module -- containing the same definitions but with explicit parameters on each -- definition. paramInstModName :: ModName -> ModName notParamInstModName :: ModName -> ModName -- | Identifiers, along with a flag that indicates whether or not they're -- infix operators. The boolean is present just as cached information -- from the lexer, and never used during comparisons. data Ident packIdent :: String -> Ident packInfix :: String -> Ident unpackIdent :: Ident -> String mkIdent :: Text -> Ident mkInfix :: Text -> Ident isInfixIdent :: Ident -> Bool nullIdent :: Ident -> Bool identText :: Ident -> Text modParamIdent :: Ident -> Ident instance GHC.Generics.Generic Cryptol.Utils.Ident.Ident instance GHC.Show.Show Cryptol.Utils.Ident.Ident instance GHC.Generics.Generic Cryptol.Utils.Ident.ModName instance GHC.Show.Show Cryptol.Utils.Ident.ModName instance GHC.Classes.Ord Cryptol.Utils.Ident.ModName instance GHC.Classes.Eq Cryptol.Utils.Ident.ModName instance GHC.Classes.Eq Cryptol.Utils.Ident.Ident instance GHC.Classes.Ord Cryptol.Utils.Ident.Ident instance Data.String.IsString Cryptol.Utils.Ident.Ident instance Control.DeepSeq.NFData Cryptol.Utils.Ident.Ident instance Control.DeepSeq.NFData Cryptol.Utils.Ident.ModName -- | A simple system so that the Cryptol driver can communicate with users -- (or not). module Cryptol.Utils.Logger -- | A logger provides simple abstraction for sending messages. data Logger -- | Log to stdout. stdoutLogger :: Logger -- | Log to stderr. stderrLogger :: Logger -- | Log to the given handle. handleLogger :: Handle -> Logger -- | A logger that ignores all messages. quietLogger :: Logger -- | Just use this function for logging. funLogger :: (String -> IO ()) -> Logger -- | Send the given string to the log. logPutStr :: Logger -> String -> IO () -- | Send the given string with a newline at the end. logPutStrLn :: Logger -> String -> IO () -- | Send the given value using its Show instance. Adds a newline at -- the end. logPrint :: Show a => Logger -> a -> IO () instance Control.DeepSeq.NFData Cryptol.Utils.Logger.Logger module Cryptol.Utils.Misc -- | Apply a function to all elements of a container. Returns -- Nothing if nothing changed, and Just container -- otherwise. anyJust :: Traversable t => (a -> Maybe a) -> t a -> Maybe (t a) -- | Apply functions to both elements of a pair. Returns Nothing if -- neither changed, and Just pair otherwise. anyJust2 :: (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b) module Cryptol.Utils.PP -- | How to display names, inspired by the GHC Outputable module. -- Getting a value of Nothing from the NameDisp function indicates -- that the display has no opinion on how this name should be displayed, -- and some other display should be tried out. data NameDisp EmptyNameDisp :: NameDisp NameDisp :: (ModName -> Ident -> Maybe NameFormat) -> NameDisp data NameFormat UnQualified :: NameFormat Qualified :: !ModName -> NameFormat NotInScope :: NameFormat -- | Never qualify names from this module. neverQualifyMod :: ModName -> NameDisp alwaysQualify :: NameDisp neverQualify :: NameDisp fmtModName :: ModName -> NameFormat -> Text -- | Compose two naming environments, preferring names from the left -- environment. extend :: NameDisp -> NameDisp -> NameDisp -- | Get the format for a name. When Nothing is returned, the name -- is not currently in scope. getNameFormat :: ModName -> Ident -> NameDisp -> NameFormat -- | Produce a document in the context of the current NameDisp. withNameDisp :: (NameDisp -> Doc) -> Doc -- | Fix the way that names are displayed inside of a doc. fixNameDisp :: NameDisp -> Doc -> Doc newtype Doc Doc :: (NameDisp -> Doc) -> Doc runDoc :: NameDisp -> Doc -> Doc render :: Doc -> String class PP a ppPrec :: PP a => Int -> a -> Doc class PP a => PPName a -- | Fixity information for infix operators ppNameFixity :: PPName a => a -> Maybe (Assoc, Int) -- | Print a name in prefix: f a b or (+) a b) ppPrefixName :: PPName a => a -> Doc -- | Print a name as an infix operator: a + b ppInfixName :: PPName a => a -> Doc pp :: PP a => a -> Doc pretty :: PP a => a -> String optParens :: Bool -> Doc -> Doc -- | Information about associativity. data Assoc LeftAssoc :: Assoc RightAssoc :: Assoc NonAssoc :: Assoc -- | Information about an infix expression of some sort. data Infix op thing Infix :: op -> thing -> thing -> Int -> Assoc -> Infix op thing -- | operator [ieOp] :: Infix op thing -> op -- | left argument [ieLeft] :: Infix op thing -> thing -- | right argumrnt [ieRight] :: Infix op thing -> thing -- | operator precedence [iePrec] :: Infix op thing -> Int -- | operator associativity [ieAssoc] :: Infix op thing -> Assoc commaSep :: [Doc] -> Doc -- | Pretty print an infix expression of some sort. ppInfix :: (PP thing, PP op) => Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc -- | Display a numeric values as an ordinar (e.g., 2nd) ordinal :: (Integral a, Show a, Eq a) => a -> Doc -- | The suffix to use when displaying a number as an oridinal ordSuffix :: (Integral a, Eq a) => a -> String liftPJ :: Doc -> Doc liftPJ1 :: (Doc -> Doc) -> Doc -> Doc liftPJ2 :: (Doc -> Doc -> Doc) -> (Doc -> Doc -> Doc) liftSep :: ([Doc] -> Doc) -> ([Doc] -> Doc) (<.>) :: Doc -> Doc -> Doc infixl 6 <.> (<+>) :: Doc -> Doc -> Doc infixl 6 <+> ($$) :: Doc -> Doc -> Doc infixl 5 $$ sep :: [Doc] -> Doc fsep :: [Doc] -> Doc hsep :: [Doc] -> Doc hcat :: [Doc] -> Doc vcat :: [Doc] -> Doc hang :: Doc -> Int -> Doc -> Doc nest :: Int -> Doc -> Doc parens :: Doc -> Doc braces :: Doc -> Doc brackets :: Doc -> Doc quotes :: Doc -> Doc punctuate :: Doc -> [Doc] -> [Doc] text :: String -> Doc char :: Char -> Doc integer :: Integer -> Doc int :: Int -> Doc comma :: Doc empty :: Doc colon :: Doc instance Control.DeepSeq.NFData Cryptol.Utils.PP.Assoc instance GHC.Generics.Generic Cryptol.Utils.PP.Assoc instance GHC.Classes.Eq Cryptol.Utils.PP.Assoc instance GHC.Show.Show Cryptol.Utils.PP.Assoc instance Control.DeepSeq.NFData Cryptol.Utils.PP.Doc instance GHC.Generics.Generic Cryptol.Utils.PP.Doc instance Control.DeepSeq.NFData Cryptol.Utils.PP.NameDisp instance GHC.Generics.Generic Cryptol.Utils.PP.NameDisp instance GHC.Show.Show Cryptol.Utils.PP.NameFormat instance Cryptol.Utils.PP.PP Data.Text.Internal.Text instance Cryptol.Utils.PP.PP Cryptol.Utils.Ident.Ident instance Cryptol.Utils.PP.PP Cryptol.Utils.Ident.ModName instance GHC.Base.Semigroup Cryptol.Utils.PP.Doc instance GHC.Base.Monoid Cryptol.Utils.PP.Doc instance GHC.Show.Show Cryptol.Utils.PP.Doc instance Data.String.IsString Cryptol.Utils.PP.Doc instance GHC.Show.Show Cryptol.Utils.PP.NameDisp instance GHC.Base.Semigroup Cryptol.Utils.PP.NameDisp instance GHC.Base.Monoid Cryptol.Utils.PP.NameDisp module Cryptol.Utils.Debug trace :: String -> b -> b ppTrace :: Doc -> b -> b module Cryptol.TypeCheck.PP type NameMap = IntMap String -- | This packages together a type with some names to be used to display -- the variables. It is used for pretty printing types. data WithNames a WithNames :: a -> NameMap -> WithNames a emptyNameMap :: NameMap ppWithNamesPrec :: PP (WithNames a) => NameMap -> Int -> a -> Doc ppWithNames :: PP (WithNames a) => NameMap -> a -> Doc -- | Expand a list of base names into an infinite list of variations. nameList :: [String] -> [String] dump :: PP (WithNames a) => a -> String module Cryptol.Parser.Selector -- | Selectors are used for projecting from various components. Each -- selector has an option spec to specify the shape of the thing that is -- being selected. Currently, there is no surface syntax for list -- selectors, but they are used during the desugaring of patterns. data Selector -- | Zero-based tuple selection. Optionally specifies the shape of the -- tuple (one-based). TupleSel :: Int -> (Maybe Int) -> Selector -- | Record selection. Optionally specifies the shape of the record. RecordSel :: Ident -> (Maybe [Ident]) -> Selector -- | List selection. Optionally specifies the length of the list. ListSel :: Int -> (Maybe Int) -> Selector -- | Display the thing selected by the selector, nicely. ppSelector :: Selector -> Doc instance Control.DeepSeq.NFData Cryptol.Parser.Selector.Selector instance GHC.Generics.Generic Cryptol.Parser.Selector.Selector instance GHC.Classes.Ord Cryptol.Parser.Selector.Selector instance GHC.Show.Show Cryptol.Parser.Selector.Selector instance GHC.Classes.Eq Cryptol.Parser.Selector.Selector instance Cryptol.Utils.PP.PP Cryptol.Parser.Selector.Selector module Cryptol.Parser.Position data Located a Located :: !Range -> !a -> Located a [srcRange] :: Located a -> !Range [thing] :: Located a -> !a data Position Position :: !Int -> !Int -> Position [line] :: Position -> !Int [col] :: Position -> !Int data Range Range :: !Position -> !Position -> FilePath -> Range [from] :: Range -> !Position [to] :: Range -> !Position [source] :: Range -> FilePath -- | An empty range. -- -- Caution: using this on the LHS of a use of rComb will cause the empty -- source to propagate. emptyRange :: Range start :: Position move :: Position -> Char -> Position moves :: Position -> Text -> Position rComb :: Range -> Range -> Range rCombs :: [Range] -> Range class HasLoc t getLoc :: HasLoc t => t -> Maybe Range class HasLoc t => AddLoc t addLoc :: AddLoc t => t -> Range -> t dropLoc :: AddLoc t => t -> t at :: (HasLoc l, AddLoc t) => l -> t -> t combLoc :: (a -> b -> c) -> Located a -> Located b -> Located c instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.Position.Located a) instance GHC.Generics.Generic (Cryptol.Parser.Position.Located a) instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.Position.Located a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.Position.Located a) instance Control.DeepSeq.NFData Cryptol.Parser.Position.Range instance GHC.Generics.Generic Cryptol.Parser.Position.Range instance GHC.Show.Show Cryptol.Parser.Position.Range instance GHC.Classes.Eq Cryptol.Parser.Position.Range instance Control.DeepSeq.NFData Cryptol.Parser.Position.Position instance GHC.Generics.Generic Cryptol.Parser.Position.Position instance GHC.Show.Show Cryptol.Parser.Position.Position instance GHC.Classes.Ord Cryptol.Parser.Position.Position instance GHC.Classes.Eq Cryptol.Parser.Position.Position instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.Position.Located a) instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.Position.Range instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.Position.Located a) instance (Cryptol.Parser.Position.HasLoc a, Cryptol.Parser.Position.HasLoc b) => Cryptol.Parser.Position.HasLoc (a, b) instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc [a] instance GHC.Base.Functor Cryptol.Parser.Position.Located instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.Position.Located a) instance Cryptol.Utils.PP.PPName a => Cryptol.Utils.PP.PPName (Cryptol.Parser.Position.Located a) instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Range instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Position module Cryptol.Parser.Fixity data Fixity Fixity :: !Assoc -> !Int -> Fixity [fAssoc] :: Fixity -> !Assoc [fLevel] :: Fixity -> !Int -- | The fixity used when none is provided. defaultFixity :: Fixity data FixityCmp FCError :: FixityCmp FCLeft :: FixityCmp FCRight :: FixityCmp compareFixity :: Fixity -> Fixity -> FixityCmp instance GHC.Classes.Eq Cryptol.Parser.Fixity.FixityCmp instance GHC.Show.Show Cryptol.Parser.Fixity.FixityCmp instance GHC.Show.Show Cryptol.Parser.Fixity.Fixity instance Control.DeepSeq.NFData Cryptol.Parser.Fixity.Fixity instance GHC.Generics.Generic Cryptol.Parser.Fixity.Fixity instance GHC.Classes.Eq Cryptol.Parser.Fixity.Fixity module Cryptol.Utils.Panic -- | Request a CallStack. -- -- NOTE: The implicit parameter ?callStack :: CallStack is an -- implementation detail and should not be considered part of the -- CallStack API, we may decide to change the implementation in -- the future. type HasCallStack = ?callStack :: CallStack type CryptolPanic = Panic Cryptol data Cryptol -- | The exception thrown when panicing. data Panic a panic :: HasCallStack => String -> [String] -> a instance Panic.PanicComponent Cryptol.Utils.Panic.Cryptol -- | This module defines natural numbers with an additional infinity -- element, and various arithmetic operators on them. module Cryptol.TypeCheck.Solver.InfNat -- | Natural numbers with an infinity element data Nat' Nat :: Integer -> Nat' Inf :: Nat' fromNat :: Nat' -> Maybe Integer nAdd :: Nat' -> Nat' -> Nat' -- | Some algebraic properties of interest: -- -- 
--   1 * x = x
--   x * (y * z) = (x * y) * z
--   0 * x = 0
--   x * y = y * x
--   x * (a + b) = x * a + x * b
--
nMul :: Nat' -> Nat' -> Nat' -- | Some algebraic properties of interest: -- -- 
--   x ^ 0        = 1
--   x ^ (n + 1)  = x * (x ^ n)
--   x ^ (m + n)  = (x ^ m) * (x ^ n)
--   x ^ (m * n)  = (x ^ m) ^ n
--
nExp :: Nat' -> Nat' -> Nat' nMin :: Nat' -> Nat' -> Nat' nMax :: Nat' -> Nat' -> Nat' -- | nSub x y = Just z iff z is the unique value such -- that Add y z = Just x. nSub :: Nat' -> Nat' -> Maybe Nat' -- | Rounds down. -- -- 
--   y * q + r = x
--   x / y     = q with remainder r
--   0 <= r && r < y
--
-- -- We don't allow Inf in the first argument for two reasons: 1. It -- matches the behavior of nMod, 2. The well-formedness -- constraints can be expressed as a conjunction. nDiv :: Nat' -> Nat' -> Maybe Nat' nMod :: Nat' -> Nat' -> Maybe Nat' -- | nCeilDiv msgLen blockSize computes the least n such -- that msgLen <= blockSize * n. It is undefined when -- blockSize = 0. It is also undefined when either input is -- infinite; perhaps this could be relaxed later. nCeilDiv :: Nat' -> Nat' -> Maybe Nat' -- | nCeilMod msgLen blockSize computes the least k such -- that blockSize divides msgLen + k. It is undefined -- when blockSize = 0. It is also undefined when either input is -- infinite; perhaps this could be relaxed later. nCeilMod :: Nat' -> Nat' -> Maybe Nat' -- | Rounds up. lg2 x = y, iff y is the smallest number -- such that x <= 2 ^ y nLg2 :: Nat' -> Nat' -- | nWidth n is number of bits needed to represent all numbers -- from 0 to n, inclusive. nWidth x = nLg2 (x + 1). nWidth :: Nat' -> Nat' -- | length ([ x, y .. ] : [_][w]) We don't check that the second -- element fits in w many bits as the second element may not be -- part of the list. For example, the length of [ 0 .. ] : -- [_][0] is nLenFromThen 0 1 0, which should evaluate to -- 1. nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat' -- | 
--   length [ x, y .. z ]
--
nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat' -- | Compute the logarithm of a number in the given base, rounded down to -- the closest integer. The boolean indicates if we the result is exact -- (i.e., True means no rounding happened, False means we rounded down). -- The logarithm base is the second argument. genLog :: Integer -> Integer -> Maybe (Integer, Bool) -- | Compute the number of bits required to represent the given integer. widthInteger :: Integer -> Integer -- | Compute the exact root of a natural number. The second argument -- specifies which root we are computing. rootExact :: Integer -> Integer -> Maybe Integer -- | Compute the the n-th root of a natural number, rounded down to the -- closest natural number. The boolean indicates if the result is exact -- (i.e., True means no rounding was done, False means rounded down). The -- second argument specifies which root we are computing. genRoot :: Integer -> Integer -> Maybe (Integer, Bool) instance Control.DeepSeq.NFData Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Show.Show Cryptol.TypeCheck.Solver.InfNat.Nat' module Cryptol.REPL.Trie -- | Maps string names to values, allowing for partial key matches and -- querying. data Trie a Node :: (Map Char (Trie a)) -> (Maybe a) -> Trie a emptyTrie :: Trie a -- | Insert a value into the Trie. Will call panic if a value -- already exists with that key. insertTrie :: String -> a -> Trie a -> Trie a -- | Return all matches with the given prefix. lookupTrie :: String -> Trie a -> [a] -- | Given a key, return either an exact match for that key, or all matches -- with the given prefix. lookupTrieExact :: String -> Trie a -> [a] -- | Return all of the values from a Trie. leaves :: Trie a -> [a] instance GHC.Show.Show a => GHC.Show.Show (Cryptol.REPL.Trie.Trie a) -- | Convert a literate source file into an ordinary source file. module Cryptol.Parser.Unlit unLit :: PreProc -> Text -> Text data PreProc None :: PreProc Markdown :: PreProc LaTeX :: PreProc guessPreProc :: FilePath -> PreProc knownExts :: [String] module Cryptol.Parser.Name -- | Names that originate in the parser. data PName -- | Unqualified names like x, Foo, or +. UnQual :: !Ident -> PName -- | Qualified names like Foo::bar or module::!. Qual :: !ModName -> !Ident -> PName -- | Fresh names generated by a pass. NewName :: !Pass -> !Int -> PName -- | Passes that can generate fresh names. data Pass NoPat :: Pass MonoValues :: Pass mkUnqual :: Ident -> PName mkQual :: ModName -> Ident -> PName getModName :: PName -> Maybe ModName getIdent :: PName -> Ident isGeneratedName :: PName -> Bool instance GHC.Generics.Generic Cryptol.Parser.Name.PName instance GHC.Show.Show Cryptol.Parser.Name.PName instance GHC.Classes.Ord Cryptol.Parser.Name.PName instance GHC.Classes.Eq Cryptol.Parser.Name.PName instance GHC.Generics.Generic Cryptol.Parser.Name.Pass instance GHC.Show.Show Cryptol.Parser.Name.Pass instance GHC.Classes.Ord Cryptol.Parser.Name.Pass instance GHC.Classes.Eq Cryptol.Parser.Name.Pass instance Control.DeepSeq.NFData Cryptol.Parser.Name.PName instance Cryptol.Utils.PP.PP Cryptol.Parser.Name.PName instance Cryptol.Utils.PP.PPName Cryptol.Parser.Name.PName instance Control.DeepSeq.NFData Cryptol.Parser.Name.Pass -- | At present Alex generates code with too many warnings. module Cryptol.Parser.Lexer -- | Returns the tokens and the last position of the input that we -- processed. The tokens include whte space tokens. primLexer :: Config -> Text -> ([Located Token], Position) -- | Returns the tokens in the last position of the input that we -- processed. White space is removed, and layout processing is done as -- requested. This stream is fed to the parser. lexer :: Config -> Text -> ([Located Token], Position) data Layout Layout :: Layout NoLayout :: Layout data Token Token :: !TokenT -> !Text -> Token [tokenType] :: Token -> !TokenT [tokenText] :: Token -> !Text data TokenT -- | value, base, number of digits Num :: !Integer -> !Int -> !Int -> TokenT -- | character literal ChrLit :: !Char -> TokenT -- | (qualified) identifier Ident :: ![Text] -> !Text -> TokenT -- | string literal StrLit :: !String -> TokenT -- | keyword KW :: !TokenKW -> TokenT -- | operator Op :: !TokenOp -> TokenT -- | symbol Sym :: !TokenSym -> TokenT -- | virtual token (for layout) Virt :: !TokenV -> TokenT -- | white space token White :: !TokenW -> TokenT -- | error token Err :: !TokenErr -> TokenT EOF :: TokenT -- | Virtual tokens, inserted by layout processing. data TokenV VCurlyL :: TokenV VCurlyR :: TokenV VSemi :: TokenV data TokenKW KW_else :: TokenKW KW_extern :: TokenKW KW_fin :: TokenKW KW_if :: TokenKW KW_private :: TokenKW KW_include :: TokenKW KW_inf :: TokenKW KW_lg2 :: TokenKW KW_lengthFromThen :: TokenKW KW_lengthFromThenTo :: TokenKW KW_max :: TokenKW KW_min :: TokenKW KW_module :: TokenKW KW_newtype :: TokenKW KW_pragma :: TokenKW KW_property :: TokenKW KW_then :: TokenKW KW_type :: TokenKW KW_where :: TokenKW KW_let :: TokenKW KW_x :: TokenKW KW_import :: TokenKW KW_as :: TokenKW KW_hiding :: TokenKW KW_infixl :: TokenKW KW_infixr :: TokenKW KW_infix :: TokenKW KW_primitive :: TokenKW KW_parameter :: TokenKW KW_constraint :: TokenKW data TokenErr UnterminatedComment :: TokenErr UnterminatedString :: TokenErr UnterminatedChar :: TokenErr InvalidString :: TokenErr InvalidChar :: TokenErr LexicalError :: TokenErr data TokenSym Bar :: TokenSym ArrL :: TokenSym ArrR :: TokenSym FatArrR :: TokenSym Lambda :: TokenSym EqDef :: TokenSym Comma :: TokenSym Semi :: TokenSym Dot :: TokenSym DotDot :: TokenSym DotDotDot :: TokenSym Colon :: TokenSym BackTick :: TokenSym ParenL :: TokenSym ParenR :: TokenSym BracketL :: TokenSym BracketR :: TokenSym CurlyL :: TokenSym CurlyR :: TokenSym TriL :: TokenSym TriR :: TokenSym Underscore :: TokenSym data TokenW BlockComment :: TokenW LineComment :: TokenW Space :: TokenW DocStr :: TokenW data Located a Located :: !Range -> !a -> Located a [srcRange] :: Located a -> !Range [thing] :: Located a -> !a data Config Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config -- | File that we are working on [cfgSource] :: Config -> !FilePath -- | Settings for layout processing [cfgLayout] :: Config -> !Layout -- | Preprocessor settings [cfgPreProc] :: Config -> PreProc -- | Implicit includes [cfgAutoInclude] :: Config -> [FilePath] -- | When we do layout processing should we add a vCurly (i.e., are we -- parsing a list of things). [cfgModuleScope] :: Config -> Bool defaultConfig :: Config module Cryptol.ModuleSystem.Name data Name -- | Information about the binding site of the name. data NameInfo -- | This name refers to a declaration from this module Declared :: !ModName -> !NameSource -> NameInfo -- | This name is a parameter (function or type) Parameter :: NameInfo data NameSource SystemName :: NameSource UserName :: NameSource nameUnique :: Name -> Int nameIdent :: Name -> Ident nameInfo :: Name -> NameInfo nameLoc :: Name -> Range nameFixity :: Name -> Maybe Fixity asPrim :: Name -> Maybe Ident -- | Compare two names lexically. cmpNameLexical :: Name -> Name -> Ordering -- | Compare two names by the way they would be displayed. cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering -- | Pretty-print a name with its source location information. ppLocName :: Name -> Doc -- | Make a new name for a declaration. mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name, Supply) -- | Make a new parameter name. mkParameter :: Ident -> Range -> Supply -> (Name, Supply) toParamInstName :: Name -> Name asParamName :: Name -> Name paramModRecParam :: Name class Monad m => FreshM m liftSupply :: FreshM m => (Supply -> (a, Supply)) -> m a -- | Retrieve the next unique from the supply. nextUniqueM :: FreshM m => m Int -- | A monad for easing the use of the supply. data SupplyT m a runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a, Supply) data Supply -- | This should only be used once at library initialization, and threaded -- through the rest of the session. The supply is started at 0x1000 to -- leave us plenty of room for names that the compiler needs to know -- about (wired-in constants). emptySupply :: Supply nextUnique :: Supply -> (Int, Supply) -- | A mapping from an identifier defined in some module to its real name. data PrimMap PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap [primDecls] :: PrimMap -> Map Ident Name [primTypes] :: PrimMap -> Map Ident Name -- | It's assumed that we're looking things up that we know already exist, -- so this will panic if it doesn't find the name. lookupPrimDecl :: Ident -> PrimMap -> Name -- | It's assumed that we're looking things up that we know already exist, -- so this will panic if it doesn't find the name. lookupPrimType :: Ident -> PrimMap -> Name instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.PrimMap instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.PrimMap instance GHC.Show.Show Cryptol.ModuleSystem.Name.PrimMap instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.Supply instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.Supply instance GHC.Show.Show Cryptol.ModuleSystem.Name.Supply instance GHC.Show.Show Cryptol.ModuleSystem.Name.Name instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.Name instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.Name instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.NameInfo instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.NameInfo instance GHC.Show.Show Cryptol.ModuleSystem.Name.NameInfo instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.NameInfo instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.NameSource instance GHC.Show.Show Cryptol.ModuleSystem.Name.NameSource instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.NameSource instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.NameSource instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.ExceptionT i m) instance (GHC.Base.Monoid i, Cryptol.ModuleSystem.Name.FreshM m) => Cryptol.ModuleSystem.Name.FreshM (MonadLib.WriterT i m) instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.ReaderT i m) instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.StateT i m) instance GHC.Base.Monad m => Cryptol.ModuleSystem.Name.FreshM (Cryptol.ModuleSystem.Name.SupplyT m) instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Name.SupplyT m) instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Name.SupplyT m) instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Name.SupplyT m) instance MonadLib.MonadT Cryptol.ModuleSystem.Name.SupplyT instance MonadLib.BaseM m n => MonadLib.BaseM (Cryptol.ModuleSystem.Name.SupplyT m) n instance MonadLib.RunM m (a, Cryptol.ModuleSystem.Name.Supply) r => MonadLib.RunM (Cryptol.ModuleSystem.Name.SupplyT m) a (Cryptol.ModuleSystem.Name.Supply -> r) instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Cryptol.ModuleSystem.Name.SupplyT m) instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.Name instance GHC.Classes.Ord Cryptol.ModuleSystem.Name.Name instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Name.Name instance Cryptol.Utils.PP.PPName Cryptol.ModuleSystem.Name.Name module Cryptol.Prims.Syntax -- | Information about a user visible built-in type. data PrimTy PrimTy :: !TCon -> !Ident -> !String -> !(Maybe Fixity) -> PrimTy -- | Use this ty-con (renamer) [primTyCon] :: PrimTy -> !TCon -- | This is what it's called [primTyIdent] :: PrimTy -> !Ident -- | Documentation [primTyDoc] :: PrimTy -> !String -- | Precedence, for infix ones [primTyFixity] :: PrimTy -> !(Maybe Fixity) -- | This list should contain all user-visible built-in types. primTyList :: [PrimTy] -- | Construct an index for quick lookup of primtys. primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy -- | Lookup a prim type by a parser name. primTyFromPName :: PName -> Maybe PrimTy -- | Lookup if a ty con is a primitive. primTyFromTC :: TCon -> Maybe PrimTy -- | Lookup a TFun prim type. primTyFromTF :: TFun -> Maybe PrimTy -- | Lookup a PC prim type. primTyFromPC :: PC -> Maybe PrimTy -- | Kinds, classify types. data Kind KType :: Kind KNum :: Kind KProp :: Kind (:->) :: Kind -> Kind -> Kind class HasKind t kindOf :: HasKind t => t -> Kind -- | Type constants. data TCon TC :: TC -> TCon PC :: PC -> TCon TF :: TFun -> TCon TError :: Kind -> TCErrorMessage -> TCon -- | Predicate symbols. If you add additional user-visible constructors, -- please update primTys. data PC -- | 
--   _ == _
--
PEqual :: PC -- | 
--   _ /= _
--
PNeq :: PC -- | 
--   _ >= _
--
PGeq :: PC -- | 
--   fin _
--
PFin :: PC -- | Has sel type field does not appear in schemas PHas :: Selector -> PC -- | 
--   Zero _
--
PZero :: PC -- | 
--   Logic _
--
PLogic :: PC -- | 
--   Arith _
--
PArith :: PC -- | 
--   Cmp _
--
PCmp :: PC -- | 
--   SignedCmp _
--
PSignedCmp :: PC -- | 
--   Literal _ _
--
PLiteral :: PC -- | This is useful when simplifying things in place PAnd :: PC -- | Ditto PTrue :: PC -- | 1-1 constants. If you add additional user-visible constructors, please -- update primTys. data TC -- | Numbers TCNum :: Integer -> TC -- | Inf TCInf :: TC -- | Bit TCBit :: TC -- | Integer TCInteger :: TC -- | 
--   Z _
--
TCIntMod :: TC -- | 
--   [_] _
--
TCSeq :: TC -- | 
--   _ -> _
--
TCFun :: TC -- | 
--   (_, _, _)
--
TCTuple :: Int -> TC -- | user-defined, T TCNewtype :: UserTC -> TC data UserTC UserTC :: Name -> Kind -> UserTC data TCErrorMessage TCErrorMessage :: !String -> TCErrorMessage [tcErrorMessage] :: TCErrorMessage -> !String -- | Built-in type functions. If you add additional user-visible -- constructors, please update primTys in -- Cryptol.Prims.Types. data TFun -- | 
--   : Num -> Num -> Num
--
TCAdd :: TFun -- | 
--   : Num -> Num -> Num
--
TCSub :: TFun -- | 
--   : Num -> Num -> Num
--
TCMul :: TFun -- | 
--   : Num -> Num -> Num
--
TCDiv :: TFun -- | 
--   : Num -> Num -> Num
--
TCMod :: TFun -- | 
--   : Num -> Num -> Num
--
TCExp :: TFun -- | 
--   : Num -> Num
--
TCWidth :: TFun -- | 
--   : Num -> Num -> Num
--
TCMin :: TFun -- | 
--   : Num -> Num -> Num
--
TCMax :: TFun -- | 
--   : Num -> Num -> Num
--
TCCeilDiv :: TFun -- | 
--   : Num -> Num -> Num
--
TCCeilMod :: TFun -- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. ] -- :: [lengthFromThen 1 5 b][b] TCLenFromThen :: TFun -- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9 -- ] :: [lengthFromThenTo 1 5 9][b] TCLenFromThenTo :: TFun instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.TCon instance GHC.Generics.Generic Cryptol.Prims.Syntax.TCon instance GHC.Classes.Ord Cryptol.Prims.Syntax.TCon instance GHC.Classes.Eq Cryptol.Prims.Syntax.TCon instance GHC.Show.Show Cryptol.Prims.Syntax.TCon instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.TFun instance GHC.Generics.Generic Cryptol.Prims.Syntax.TFun instance GHC.Enum.Enum Cryptol.Prims.Syntax.TFun instance GHC.Enum.Bounded Cryptol.Prims.Syntax.TFun instance GHC.Classes.Ord Cryptol.Prims.Syntax.TFun instance GHC.Classes.Eq Cryptol.Prims.Syntax.TFun instance GHC.Show.Show Cryptol.Prims.Syntax.TFun instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.TCErrorMessage instance GHC.Generics.Generic Cryptol.Prims.Syntax.TCErrorMessage instance GHC.Classes.Ord Cryptol.Prims.Syntax.TCErrorMessage instance GHC.Classes.Eq Cryptol.Prims.Syntax.TCErrorMessage instance GHC.Show.Show Cryptol.Prims.Syntax.TCErrorMessage instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.TC instance GHC.Generics.Generic Cryptol.Prims.Syntax.TC instance GHC.Classes.Ord Cryptol.Prims.Syntax.TC instance GHC.Classes.Eq Cryptol.Prims.Syntax.TC instance GHC.Show.Show Cryptol.Prims.Syntax.TC instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.UserTC instance GHC.Generics.Generic Cryptol.Prims.Syntax.UserTC instance GHC.Show.Show Cryptol.Prims.Syntax.UserTC instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.PC instance GHC.Generics.Generic Cryptol.Prims.Syntax.PC instance GHC.Classes.Ord Cryptol.Prims.Syntax.PC instance GHC.Classes.Eq Cryptol.Prims.Syntax.PC instance GHC.Show.Show Cryptol.Prims.Syntax.PC instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.Kind instance GHC.Generics.Generic Cryptol.Prims.Syntax.Kind instance GHC.Show.Show Cryptol.Prims.Syntax.Kind instance GHC.Classes.Ord Cryptol.Prims.Syntax.Kind instance GHC.Classes.Eq Cryptol.Prims.Syntax.Kind instance GHC.Classes.Eq Cryptol.Prims.Syntax.PrimTy instance GHC.Classes.Ord Cryptol.Prims.Syntax.PrimTy instance Cryptol.Utils.PP.PPName Cryptol.Prims.Syntax.TFun instance Cryptol.Prims.Syntax.HasKind Cryptol.Prims.Syntax.TCon instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TCon instance Cryptol.Utils.PP.PPName Cryptol.Prims.Syntax.TCon instance Cryptol.Prims.Syntax.HasKind Cryptol.Prims.Syntax.TFun instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TFun instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TCErrorMessage instance Cryptol.Prims.Syntax.HasKind Cryptol.Prims.Syntax.TC instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TC instance Cryptol.Prims.Syntax.HasKind Cryptol.Prims.Syntax.UserTC instance GHC.Classes.Eq Cryptol.Prims.Syntax.UserTC instance GHC.Classes.Ord Cryptol.Prims.Syntax.UserTC instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.UserTC instance Cryptol.Prims.Syntax.HasKind Cryptol.Prims.Syntax.PC instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.PC instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.Kind module Cryptol.TypeCheck.Type class FVS t fvs :: FVS t => t -> Set TVar -- | The type is "simple" (i.e., it contains no type functions). type SType = Type -- | Named records data Newtype Newtype :: Name -> [TParam] -> [Prop] -> [(Ident, Type)] -> Maybe String -> Newtype [ntName] :: Newtype -> Name [ntParams] :: Newtype -> [TParam] [ntConstraints] :: Newtype -> [Prop] [ntFields] :: Newtype -> [(Ident, Type)] [ntDoc] :: Newtype -> Maybe String -- | Type synonym. data TySyn TySyn :: Name -> [TParam] -> [Prop] -> Type -> !(Maybe String) -> TySyn -- | Name [tsName] :: TySyn -> Name -- | Parameters [tsParams] :: TySyn -> [TParam] -- | Ensure body is OK [tsConstraints] :: TySyn -> [Prop] -- | Definition [tsDef] :: TySyn -> Type -- | Documentation [tsDoc] :: TySyn -> !(Maybe String) -- | The type is supposed to be of kind KProp type Prop = Type data TVarSource -- | Name of module parameter TVFromModParam :: Name -> TVarSource -- | A variable in a signature TVFromSignature :: Name -> TVarSource TypeWildCard :: TVarSource TypeOfRecordField :: Ident -> TVarSource TypeOfTupleField :: Int -> TVarSource TypeOfSeqElement :: TVarSource LenOfSeq :: TVarSource TypeParamInstNamed :: Name -> Ident -> TVarSource TypeParamInstPos :: Name -> Int -> TVarSource DefinitionOf :: Name -> TVarSource LenOfCompGen :: TVarSource TypeOfArg :: (Maybe Int) -> TVarSource TypeOfRes :: TVarSource TypeErrorPlaceHolder :: TVarSource data TVarInfo TVarInfo :: Range -> TVarSource -> TVarInfo -- | Source code that gave rise [tvarSource] :: TVarInfo -> Range -- | Description [tvarDesc] :: TVarInfo -> TVarSource -- | Type variables. data TVar -- | Unique, kind, ids of bound type variables that are in scope The last -- field gives us some infor for nicer warnings/errors. TVFree :: !Int -> Kind -> (Set TParam) -> TVarInfo -> TVar TVBound :: {-# UNPACK #-} !TParam -> TVar -- | The internal representation of types. These are assumed to be kind -- correct. data Type -- | Type constant with args TCon :: !TCon -> ![Type] -> Type -- | Type variable (free or bound) TVar :: TVar -> Type -- | This is just a type annotation, for a type that was written as a type -- synonym. It is useful so that we can use it to report nicer errors. -- Example: `TUser T ts t` is really just the type t that was -- written as `T ts` by the user. TUser :: !Name -> ![Type] -> !Type -> Type -- | Record type TRec :: ![(Ident, Type)] -> Type data TPFlavor TPModParam :: Name -> TPFlavor TPOther :: (Maybe Name) -> TPFlavor -- | Type parameters. data TParam TParam :: !Int -> Kind -> TPFlavor -> !TVarInfo -> TParam -- | Parameter identifier [tpUnique] :: TParam -> !Int -- | Kind of parameter [tpKind] :: TParam -> Kind -- | What sort of type parameter is this [tpFlav] :: TParam -> TPFlavor -- | A description for better messages. [tpInfo] :: TParam -> !TVarInfo -- | The types of polymorphic values. data Schema Forall :: [TParam] -> [Prop] -> Type -> Schema [sVars] :: Schema -> [TParam] [sProps] :: Schema -> [Prop] [sType] :: Schema -> Type tMono :: Type -> Schema isMono :: Schema -> Maybe Type schemaParam :: Name -> TPFlavor tySynParam :: Name -> TPFlavor propSynParam :: Name -> TPFlavor newtypeParam :: Name -> TPFlavor modTyParam :: Name -> TPFlavor tpfName :: TPFlavor -> Maybe Name tpName :: TParam -> Maybe Name tvInfo :: TVar -> TVarInfo -- | Get the names of something that is related to the tvar. tvSourceName :: TVarSource -> Maybe Name quickApply :: Kind -> [a] -> Kind kindResult :: Kind -> Kind tpVar :: TParam -> TVar newtypeConType :: Newtype -> Schema isFreeTV :: TVar -> Bool isBoundTV :: TVar -> Bool tIsError :: Type -> Maybe TCErrorMessage tIsNat' :: Type -> Maybe Nat' tIsNum :: Type -> Maybe Integer tIsInf :: Type -> Bool tIsVar :: Type -> Maybe TVar tIsFun :: Type -> Maybe (Type, Type) tIsSeq :: Type -> Maybe (Type, Type) tIsBit :: Type -> Bool tIsInteger :: Type -> Bool tIsIntMod :: Type -> Maybe Type tIsTuple :: Type -> Maybe [Type] tIsRec :: Type -> Maybe [(Ident, Type)] tIsBinFun :: TFun -> Type -> Maybe (Type, Type) -- | Split up repeated occurances of the given binary type-level function. tSplitFun :: TFun -> Type -> [Type] pIsFin :: Prop -> Maybe Type pIsGeq :: Prop -> Maybe (Type, Type) pIsEq :: Prop -> Maybe (Type, Type) pIsZero :: Prop -> Maybe Type pIsLogic :: Prop -> Maybe Type pIsArith :: Prop -> Maybe Type pIsCmp :: Prop -> Maybe Type pIsSignedCmp :: Prop -> Maybe Type pIsLiteral :: Prop -> Maybe (Type, Type) pIsTrue :: Prop -> Bool pIsWidth :: Prop -> Maybe Type tNum :: Integral a => a -> Type tZero :: Type tOne :: Type tTwo :: Type tInf :: Type tNat' :: Nat' -> Type tBit :: Type tInteger :: Type tIntMod :: Type -> Type tWord :: Type -> Type tSeq :: Type -> Type -> Type tChar :: Type tString :: Int -> Type tRec :: [(Ident, Type)] -> Type tTuple :: [Type] -> Type newtypeTyCon :: Newtype -> TCon -- | Make a function type. tFun :: Type -> Type -> Type infixr 5 `tFun` -- | Eliminate outermost type synonyms. tNoUser :: Type -> Type -- | Make a malformed numeric type. tBadNumber :: TCErrorMessage -> Type tf1 :: TFun -> Type -> Type tf2 :: TFun -> Type -> Type -> Type tf3 :: TFun -> Type -> Type -> Type -> Type tSub :: Type -> Type -> Type tMul :: Type -> Type -> Type tDiv :: Type -> Type -> Type tMod :: Type -> Type -> Type tExp :: Type -> Type -> Type tMin :: Type -> Type -> Type tCeilDiv :: Type -> Type -> Type tCeilMod :: Type -> Type -> Type tLenFromThen :: Type -> Type -> Type -> Type tLenFromThenTo :: Type -> Type -> Type -> Type -- | Equality for numeric types. (=#=) :: Type -> Type -> Prop infix 4 =#= (=/=) :: Type -> Type -> Prop pZero :: Type -> Prop pLogic :: Type -> Prop pArith :: Type -> Prop pCmp :: Type -> Prop pSignedCmp :: Type -> Prop pLiteral :: Type -> Type -> Prop -- | Make a greater-than-or-equal-to constraint. (>==) :: Type -> Type -> Prop infix 4 >== -- | A Has constraint, used for tuple and record selection. pHas :: Selector -> Type -> Type -> Prop pTrue :: Prop pAnd :: [Prop] -> Prop pSplitAnd :: Prop -> [Prop] pFin :: Type -> Prop -- | Make a malformed property. pError :: TCErrorMessage -> Prop noFreeVariables :: FVS t => t -> Bool addTNames :: [TParam] -> NameMap -> NameMap ppNewtypeShort :: Newtype -> Doc pickTVarName :: Kind -> TVarSource -> Int -> Doc instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Newtype instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Newtype instance GHC.Show.Show Cryptol.TypeCheck.Type.Newtype instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TySyn instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TySyn instance GHC.Show.Show Cryptol.TypeCheck.Type.TySyn instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Schema instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Schema instance GHC.Show.Show Cryptol.TypeCheck.Type.Schema instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Schema instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Type instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Type instance GHC.Show.Show Cryptol.TypeCheck.Type.Type instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVar instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVar instance GHC.Show.Show Cryptol.TypeCheck.Type.TVar instance GHC.Show.Show Cryptol.TypeCheck.Type.TParam instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TParam instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TParam instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVarInfo instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVarInfo instance GHC.Show.Show Cryptol.TypeCheck.Type.TVarInfo instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVarSource instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVarSource instance GHC.Show.Show Cryptol.TypeCheck.Type.TVarSource instance GHC.Show.Show Cryptol.TypeCheck.Type.TPFlavor instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TPFlavor instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TPFlavor instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Type instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS (GHC.Base.Maybe a) instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS [a] instance (Cryptol.TypeCheck.Type.FVS a, Cryptol.TypeCheck.Type.FVS b) => Cryptol.TypeCheck.Type.FVS (a, b) instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Schema instance Cryptol.Prims.Syntax.HasKind Cryptol.TypeCheck.Type.Newtype instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Newtype instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Newtype) instance Cryptol.Prims.Syntax.HasKind Cryptol.TypeCheck.Type.TySyn instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TySyn instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TySyn) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Schema instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Schema) instance Cryptol.Prims.Syntax.HasKind Cryptol.TypeCheck.Type.Type instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Type instance GHC.Classes.Ord Cryptol.TypeCheck.Type.Type instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Type) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Type instance Cryptol.Prims.Syntax.HasKind Cryptol.TypeCheck.Type.TVar instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TVar instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TVar instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TVar) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVar instance Cryptol.Prims.Syntax.HasKind Cryptol.TypeCheck.Type.TParam instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TParam instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TParam instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TParam instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TParam) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVarInfo instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVarSource module Cryptol.Parser.AST -- | Identifiers, along with a flag that indicates whether or not they're -- infix operators. The boolean is present just as cached information -- from the lexer, and never used during comparisons. data Ident mkIdent :: Text -> Ident mkInfix :: Text -> Ident isInfixIdent :: Ident -> Bool nullIdent :: Ident -> Bool identText :: Ident -> Text -- | Module names are just text. data ModName modRange :: Module name -> Range -- | Names that originate in the parser. data PName -- | Unqualified names like x, Foo, or +. UnQual :: !Ident -> PName -- | Qualified names like Foo::bar or module::!. Qual :: !ModName -> !Ident -> PName -- | Fresh names generated by a pass. NewName :: !Pass -> !Int -> PName getModName :: PName -> Maybe ModName getIdent :: PName -> Ident mkUnqual :: Ident -> PName mkQual :: ModName -> Ident -> PName data Named a Named :: Located Ident -> a -> Named a [name] :: Named a -> Located Ident [value] :: Named a -> a -- | Passes that can generate fresh names. data Pass NoPat :: Pass MonoValues :: Pass -- | Information about associativity. data Assoc LeftAssoc :: Assoc RightAssoc :: Assoc NonAssoc :: Assoc data Schema n Forall :: [TParam n] -> [Prop n] -> (Type n) -> (Maybe Range) -> Schema n data TParam n TParam :: n -> Maybe Kind -> Maybe Range -> TParam n [tpName] :: TParam n -> n [tpKind] :: TParam n -> Maybe Kind [tpRange] :: TParam n -> Maybe Range data Kind KNum :: Kind KType :: Kind KFun :: Kind -> Kind -> Kind data Type n -- | 
--   [8] -> [8]
--
TFun :: (Type n) -> (Type n) -> Type n -- | 
--   [8] a
--
TSeq :: (Type n) -> (Type n) -> Type n -- | 
--   Bit
--
TBit :: Type n -- | 
--   10
--
TNum :: Integer -> Type n -- | 
--   a
--
TChar :: Char -> Type n -- | A type variable or synonym TUser :: n -> [Type n] -> Type n -- | 2 + x Note that the parser never produces these; instead it -- produces a TUser value. The TApp is introduced by the -- renamer when it spots built-in functions. XXX: We should just add -- primitive declarations for the built-in type functions, and simplify -- all this. TApp :: TCon -> [Type n] -> Type n -- | 
--   { x : [8], y : [32] }
--
TRecord :: [Named (Type n)] -> Type n -- | 
--   ([8], [32])
--
TTuple :: [Type n] -> Type n -- | _, just some type. TWild :: Type n -- | Location information TLocated :: (Type n) -> Range -> Type n -- | 
--   (ty)
--
TParens :: (Type n) -> Type n -- | 
--   ty + ty
--
TInfix :: (Type n) -> (Located n) -> Fixity -> (Type n) -> Type n data Prop n -- | 
--   fin x
--
CFin :: (Type n) -> Prop n -- | 
--   x == 10
--
CEqual :: (Type n) -> (Type n) -> Prop n -- | 
--   x != 10
--
CNeq :: (Type n) -> (Type n) -> Prop n -- | 
--   x >= 10
--
CGeq :: (Type n) -> (Type n) -> Prop n -- | 
--   Zero a
--
CZero :: (Type n) -> Prop n -- | 
--   Logic a
--
CLogic :: (Type n) -> Prop n -- | 
--   Arith a
--
CArith :: (Type n) -> Prop n -- | 
--   Cmp a
--
CCmp :: (Type n) -> Prop n -- | 
--   SignedCmp a
--
CSignedCmp :: (Type n) -> Prop n -- | 
--   Literal val a
--
CLiteral :: (Type n) -> (Type n) -> Prop n -- | Constraint synonym CUser :: n -> [Type n] -> Prop n -- | Location information CLocated :: (Prop n) -> Range -> Prop n -- | After parsing CType :: (Type n) -> Prop n -- | A parsed module. data Module name Module :: Located ModName -> !(Maybe (Located ModName)) -> [Located Import] -> [TopDecl name] -> Module name -- | Name of the module [mName] :: Module name -> Located ModName -- | Functor to instantiate (if this is a functor instnaces) [mInstance] :: Module name -> !(Maybe (Located ModName)) -- | Imports for the module [mImports] :: Module name -> [Located Import] -- | Declartions for the module [mDecls] :: Module name -> [TopDecl name] newtype Program name Program :: [TopDecl name] -> Program name data TopDecl name Decl :: (TopLevel (Decl name)) -> TopDecl name -- | @newtype T as = t TDNewtype :: (TopLevel (Newtype name)) -> TopDecl name -- | 
--   include File
--
Include :: (Located FilePath) -> TopDecl name -- | 
--   parameter type T : #
--
DParameterType :: (ParameterType name) -> TopDecl name -- | 
--   parameter type constraint (fin T)
--
DParameterConstraint :: [Located (Prop name)] -> TopDecl name -- | 
--   parameter someVal : [256]
--
DParameterFun :: (ParameterFun name) -> TopDecl name data Decl name DSignature :: [Located name] -> (Schema name) -> Decl name DFixity :: !Fixity -> [Located name] -> Decl name DPragma :: [Located name] -> Pragma -> Decl name DBind :: (Bind name) -> Decl name DPatBind :: (Pattern name) -> (Expr name) -> Decl name DType :: (TySyn name) -> Decl name DProp :: (PropSyn name) -> Decl name DLocated :: (Decl name) -> Range -> Decl name data Fixity Fixity :: !Assoc -> !Int -> Fixity [fAssoc] :: Fixity -> !Assoc [fLevel] :: Fixity -> !Int -- | The fixity used when none is provided. defaultFixity :: Fixity data FixityCmp FCError :: FixityCmp FCLeft :: FixityCmp FCRight :: FixityCmp compareFixity :: Fixity -> Fixity -> FixityCmp data TySyn n TySyn :: (Located n) -> [TParam n] -> (Type n) -> TySyn n data PropSyn n PropSyn :: (Located n) -> [TParam n] -> [Prop n] -> PropSyn n -- | Bindings. Notes: -- -- data Bind name Bind :: Located name -> [Pattern name] -> Located (BindDef name) -> Maybe (Schema name) -> Bool -> Maybe Fixity -> [Pragma] -> Bool -> Maybe String -> Bind name -- | Defined thing [bName] :: Bind name -> Located name -- | Parameters [bParams] :: Bind name -> [Pattern name] -- | Definition [bDef] :: Bind name -> Located (BindDef name) -- | Optional type sig [bSignature] :: Bind name -> Maybe (Schema name) -- | Infix operator? [bInfix] :: Bind name -> Bool -- | Optional fixity info [bFixity] :: Bind name -> Maybe Fixity -- | Optional pragmas [bPragmas] :: Bind name -> [Pragma] -- | Is this a monomorphic binding [bMono] :: Bind name -> Bool -- | Optional doc string [bDoc] :: Bind name -> Maybe String data BindDef name DPrim :: BindDef name DExpr :: (Expr name) -> BindDef name type LBindDef = Located (BindDef PName) data Pragma PragmaNote :: String -> Pragma PragmaProperty :: Pragma -- | Export information for a declaration. data ExportType Public :: ExportType Private :: ExportType -- | A top-level module declaration. data TopLevel a TopLevel :: ExportType -> Maybe (Located String) -> a -> TopLevel a [tlExport] :: TopLevel a -> ExportType [tlDoc] :: TopLevel a -> Maybe (Located String) [tlValue] :: TopLevel a -> a -- | An import declaration. data Import Import :: !ModName -> Maybe ModName -> Maybe ImportSpec -> Import [iModule] :: Import -> !ModName [iAs] :: Import -> Maybe ModName [iSpec] :: Import -> Maybe ImportSpec -- | The list of names following an import. -- -- INVARIANT: All of the Name entries in the list are expected -- to be unqualified names; the QName or NewName -- constructors should not be present. data ImportSpec Hiding :: [Ident] -> ImportSpec Only :: [Ident] -> ImportSpec data Newtype name Newtype :: Located name -> [TParam name] -> [Named (Type name)] -> Newtype name -- | Type name [nName] :: Newtype name -> Located name -- | Type params [nParams] :: Newtype name -> [TParam name] -- | Constructor [nBody] :: Newtype name -> [Named (Type name)] -- | A type parameter data ParameterType name ParameterType :: Located name -> Kind -> Maybe String -> Maybe Fixity -> !Int -> ParameterType name -- | name of type parameter [ptName] :: ParameterType name -> Located name -- | kind of parameter [ptKind] :: ParameterType name -> Kind -- | optional documentation [ptDoc] :: ParameterType name -> Maybe String -- | info for infix use [ptFixity] :: ParameterType name -> Maybe Fixity -- | number of the parameter [ptNumber] :: ParameterType name -> !Int -- | A value parameter data ParameterFun name ParameterFun :: Located name -> Schema name -> Maybe String -> Maybe Fixity -> ParameterFun name -- | name of value parameter [pfName] :: ParameterFun name -> Located name -- | schema for parameter [pfSchema] :: ParameterFun name -> Schema name -- | optional documentation [pfDoc] :: ParameterFun name -> Maybe String -- | info for infix use [pfFixity] :: ParameterFun name -> Maybe Fixity -- | Input at the REPL, which can either be an expression or a let -- statement. data ReplInput name ExprInput :: (Expr name) -> ReplInput name LetInput :: (Decl name) -> ReplInput name data Expr n -- | 
--   x
--
EVar :: n -> Expr n -- | 
--   0x10
--
ELit :: Literal -> Expr n -- | 
--   -1
--
ENeg :: (Expr n) -> Expr n -- | 
--   ~1
--
EComplement :: (Expr n) -> Expr n -- | 
--   (1,2,3)
--
ETuple :: [Expr n] -> Expr n -- | 
--   { x = 1, y = 2 }
--
ERecord :: [Named (Expr n)] -> Expr n -- | 
--   e.l
--
ESel :: (Expr n) -> Selector -> Expr n -- | 
--   [1,2,3]
--
EList :: [Expr n] -> Expr n -- | 
--   [1, 5 ..  117 ]
--
EFromTo :: (Type n) -> (Maybe (Type n)) -> (Maybe (Type n)) -> Expr n -- | 
--   [1, 3 ...]
--
EInfFrom :: (Expr n) -> (Maybe (Expr n)) -> Expr n -- | 
--   [ 1 | x <- xs ]
--
EComp :: (Expr n) -> [[Match n]] -> Expr n -- | 
--   f x
--
EApp :: (Expr n) -> (Expr n) -> Expr n -- | 
--   f `{x = 8}, f`{8}
--
EAppT :: (Expr n) -> [(TypeInst n)] -> Expr n -- | 
--   if ok then e1 else e2
--
EIf :: (Expr n) -> (Expr n) -> (Expr n) -> Expr n -- | 
--   1 + x where { x = 2 }
--
EWhere :: (Expr n) -> [Decl n] -> Expr n -- | 
--   1 : [8]
--
ETyped :: (Expr n) -> (Type n) -> Expr n -- | `(x + 1), x is a type ETypeVal :: (Type n) -> Expr n -- | 
--   \x y -> x
--
EFun :: [Pattern n] -> (Expr n) -> Expr n -- | position annotation ELocated :: (Expr n) -> Range -> Expr n -- | (e) (Removed by Fixity) EParens :: (Expr n) -> Expr n -- | a + b (Removed by Fixity) EInfix :: (Expr n) -> (Located n) -> Fixity -> (Expr n) -> Expr n -- | Literals. data Literal -- | 0x10 (HexLit 2) ECNum :: Integer -> NumInfo -> Literal -- | 
--   "hello"
--
ECString :: String -> Literal -- | Infromation about the representation of a numeric constant. data NumInfo -- | n-digit binary literal BinLit :: Int -> NumInfo -- | n-digit octal literal OctLit :: Int -> NumInfo -- | overloaded decimal literal DecLit :: NumInfo -- | n-digit hex literal HexLit :: Int -> NumInfo -- | character literal CharLit :: NumInfo -- | polynomial literal PolyLit :: Int -> NumInfo data Match name -- | p <- e Match :: (Pattern name) -> (Expr name) -> Match name MatchLet :: (Bind name) -> Match name data Pattern n -- | 
--   x
--
PVar :: (Located n) -> Pattern n -- | 
--   _
--
PWild :: Pattern n -- | 
--   (x,y,z)
--
PTuple :: [Pattern n] -> Pattern n -- | 
--   { x = (a,b,c), y = z }
--
PRecord :: [Named (Pattern n)] -> Pattern n -- | 
--   [ x, y, z ]
--
PList :: [Pattern n] -> Pattern n -- | 
--   x : [8]
--
PTyped :: (Pattern n) -> (Type n) -> Pattern n -- | 
--   (x # y)
--
PSplit :: (Pattern n) -> (Pattern n) -> Pattern n -- | Location information PLocated :: (Pattern n) -> Range -> Pattern n -- | Selectors are used for projecting from various components. Each -- selector has an option spec to specify the shape of the thing that is -- being selected. Currently, there is no surface syntax for list -- selectors, but they are used during the desugaring of patterns. data Selector -- | Zero-based tuple selection. Optionally specifies the shape of the -- tuple (one-based). TupleSel :: Int -> (Maybe Int) -> Selector -- | Record selection. Optionally specifies the shape of the record. RecordSel :: Ident -> (Maybe [Ident]) -> Selector -- | List selection. Optionally specifies the length of the list. ListSel :: Int -> (Maybe Int) -> Selector data TypeInst name NamedInst :: (Named (Type name)) -> TypeInst name PosInst :: (Type name) -> TypeInst name data Located a Located :: !Range -> !a -> Located a [srcRange] :: Located a -> !Range [thing] :: Located a -> !a -- | A name with location information. type LPName = Located PName -- | A string with location information. type LString = Located String -- | An identifier with location information. type LIdent = Located Ident class NoPos t noPos :: NoPos t => t -> t -- | Conversational printing of kinds (e.g., to use in error -- messages) cppKind :: Kind -> Doc -- | Display the thing selected by the selector, nicely. ppSelector :: Selector -> Doc instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Program name) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Module name) instance GHC.Generics.Generic (Cryptol.Parser.AST.Module name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Module name) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopDecl name) instance GHC.Generics.Generic (Cryptol.Parser.AST.TopDecl name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TopDecl name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ReplInput name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ReplInput name) instance GHC.Base.Functor Cryptol.Parser.AST.BindDef instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.BindDef name) instance GHC.Generics.Generic (Cryptol.Parser.AST.BindDef name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.BindDef name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.BindDef name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Bind name) instance GHC.Base.Functor Cryptol.Parser.AST.Bind instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Bind name) instance GHC.Generics.Generic (Cryptol.Parser.AST.Bind name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Bind name) instance GHC.Base.Functor Cryptol.Parser.AST.Match instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Match name) instance GHC.Generics.Generic (Cryptol.Parser.AST.Match name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Match name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Match name) instance GHC.Base.Functor Cryptol.Parser.AST.Expr instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Expr n) instance GHC.Generics.Generic (Cryptol.Parser.AST.Expr n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Expr n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Expr n) instance GHC.Base.Functor Cryptol.Parser.AST.Decl instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Decl name) instance GHC.Generics.Generic (Cryptol.Parser.AST.Decl name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Decl name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Decl name) instance GHC.Base.Functor Cryptol.Parser.AST.PropSyn instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.PropSyn n) instance GHC.Generics.Generic (Cryptol.Parser.AST.PropSyn n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.PropSyn n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.PropSyn n) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.ParameterFun name) instance GHC.Generics.Generic (Cryptol.Parser.AST.ParameterFun name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ParameterFun name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ParameterFun name) instance GHC.Base.Functor Cryptol.Parser.AST.Schema instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Schema n) instance GHC.Generics.Generic (Cryptol.Parser.AST.Schema n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Schema n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Schema n) instance GHC.Base.Functor Cryptol.Parser.AST.Prop instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Prop n) instance GHC.Generics.Generic (Cryptol.Parser.AST.Prop n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Prop n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Prop n) instance GHC.Base.Functor Cryptol.Parser.AST.TySyn instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TySyn n) instance GHC.Generics.Generic (Cryptol.Parser.AST.TySyn n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TySyn n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TySyn n) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Newtype name) instance GHC.Generics.Generic (Cryptol.Parser.AST.Newtype name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Newtype name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Newtype name) instance GHC.Base.Functor Cryptol.Parser.AST.TypeInst instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TypeInst name) instance GHC.Generics.Generic (Cryptol.Parser.AST.TypeInst name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TypeInst name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.TypeInst name) instance GHC.Base.Functor Cryptol.Parser.AST.Pattern instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Pattern n) instance GHC.Generics.Generic (Cryptol.Parser.AST.Pattern n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Pattern n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Pattern n) instance GHC.Base.Functor Cryptol.Parser.AST.Type instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Type n) instance GHC.Generics.Generic (Cryptol.Parser.AST.Type n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Type n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Type n) instance GHC.Base.Functor Cryptol.Parser.AST.TParam instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TParam n) instance GHC.Generics.Generic (Cryptol.Parser.AST.TParam n) instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TParam n) instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TParam n) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.ParameterType name) instance GHC.Generics.Generic (Cryptol.Parser.AST.ParameterType name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ParameterType name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ParameterType name) instance Control.DeepSeq.NFData Cryptol.Parser.AST.Kind instance GHC.Generics.Generic Cryptol.Parser.AST.Kind instance GHC.Show.Show Cryptol.Parser.AST.Kind instance GHC.Classes.Eq Cryptol.Parser.AST.Kind instance GHC.Base.Functor Cryptol.Parser.AST.Named instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.Named a) instance GHC.Generics.Generic (Cryptol.Parser.AST.Named a) instance Data.Traversable.Traversable Cryptol.Parser.AST.Named instance Data.Foldable.Foldable Cryptol.Parser.AST.Named instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.Named a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.Named a) instance Control.DeepSeq.NFData Cryptol.Parser.AST.Literal instance GHC.Generics.Generic Cryptol.Parser.AST.Literal instance GHC.Show.Show Cryptol.Parser.AST.Literal instance GHC.Classes.Eq Cryptol.Parser.AST.Literal instance Control.DeepSeq.NFData Cryptol.Parser.AST.NumInfo instance GHC.Generics.Generic Cryptol.Parser.AST.NumInfo instance GHC.Show.Show Cryptol.Parser.AST.NumInfo instance GHC.Classes.Eq Cryptol.Parser.AST.NumInfo instance Data.Traversable.Traversable Cryptol.Parser.AST.TopLevel instance Data.Foldable.Foldable Cryptol.Parser.AST.TopLevel instance GHC.Base.Functor Cryptol.Parser.AST.TopLevel instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopLevel a) instance GHC.Generics.Generic (Cryptol.Parser.AST.TopLevel a) instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.TopLevel a) instance Control.DeepSeq.NFData Cryptol.Parser.AST.ExportType instance GHC.Generics.Generic Cryptol.Parser.AST.ExportType instance GHC.Classes.Ord Cryptol.Parser.AST.ExportType instance GHC.Show.Show Cryptol.Parser.AST.ExportType instance GHC.Classes.Eq Cryptol.Parser.AST.ExportType instance Control.DeepSeq.NFData Cryptol.Parser.AST.Pragma instance GHC.Generics.Generic Cryptol.Parser.AST.Pragma instance GHC.Show.Show Cryptol.Parser.AST.Pragma instance GHC.Classes.Eq Cryptol.Parser.AST.Pragma instance Control.DeepSeq.NFData Cryptol.Parser.AST.Import instance GHC.Generics.Generic Cryptol.Parser.AST.Import instance GHC.Show.Show Cryptol.Parser.AST.Import instance GHC.Classes.Eq Cryptol.Parser.AST.Import instance Control.DeepSeq.NFData Cryptol.Parser.AST.ImportSpec instance GHC.Generics.Generic Cryptol.Parser.AST.ImportSpec instance GHC.Show.Show Cryptol.Parser.AST.ImportSpec instance GHC.Classes.Eq Cryptol.Parser.AST.ImportSpec instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.Position.Located t) instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Named t) instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos [t] instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (GHC.Base.Maybe t) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Program name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Module name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopDecl name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.ParameterType name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.ParameterFun x) instance Cryptol.Parser.AST.NoPos a => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Decl name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Newtype name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Bind name) instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pragma instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TySyn name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.PropSyn name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Expr name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TypeInst name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Match name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Pattern name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Schema name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TParam name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Type name) instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Prop name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Program name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Module name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Module name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopDecl name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopDecl name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Expr n) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Expr name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Bind name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Match name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Decl name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Decl name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Decl name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Bind name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.BindDef name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Expr name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Match name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.PropSyn name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.ParameterFun name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.ParameterFun name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Schema name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Schema name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Schema name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Prop name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Prop name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Prop name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TySyn name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Newtype name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Newtype name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TypeInst name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Pattern name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Pattern name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Pattern name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Type name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Type name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Type name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TParam name) instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.TParam name) instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TParam name) instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.ParameterType name) instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.ParameterType name) instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Kind instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Named a) instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Literal instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pragma instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Import instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ImportSpec -- | This module defines the scoping rules for value- and type-level names -- in Cryptol. module Cryptol.Parser.Names -- | The names defined by a newtype. tnamesNT :: Newtype name -> ([Located name], ()) -- | The names defined and used by a group of mutually recursive -- declarations. namesDs :: Ord name => [Decl name] -> ([Located name], Set name) -- | The names defined and used by a single declarations. namesD :: Ord name => Decl name -> ([Located name], Set name) -- | The names defined and used by a single declarations in such a way that -- they cannot be duplicated in a file. For example, it is fine to use -- x on the RHS of two bindings, but not on the LHS of two type -- signatures. allNamesD :: Ord name => Decl name -> [Located name] tsName :: TySyn name -> Located name psName :: PropSyn name -> Located name -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name) namesDef :: Ord name => BindDef name -> Set name -- | The names used by an expression. namesE :: Ord name => Expr name -> Set name -- | The names defined by a group of patterns. namesPs :: [Pattern name] -> [Located name] -- | The names defined by a pattern. These will always be unqualified -- names. namesP :: Pattern name -> [Located name] -- | The names defined and used by a match. namesM :: Ord name => Match name -> ([Located name], Set name) -- | The names defined and used by an arm of alist comprehension. namesArm :: Ord name => [Match name] -> ([Located name], Set name) -- | Remove some defined variables from a set of free variables. boundNames :: Ord name => [Located name] -> Set name -> Set name -- | Given the set of type variables that are in scope, compute the type -- synonyms used by a type. namesT :: Ord name => Set name -> Type name -> Set name -- | Given the set of type variables that are in scope, compute the -- type/constraint synonyms used by a prop. namesC :: Ord name => Set name -> Prop name -> Set name -- | The type names defined and used by a group of mutually recursive -- declarations. tnamesDs :: Ord name => [Decl name] -> ([Located name], Set name) -- | The type names defined and used by a single declaration. tnamesD :: Ord name => Decl name -> ([Located name], Set name) -- | The type names used by a single binding. tnamesB :: Ord name => Bind name -> Set name tnamesDef :: Ord name => BindDef name -> Set name -- | The type names used by an expression. tnamesE :: Ord name => Expr name -> Set name tnamesTI :: Ord name => TypeInst name -> Set name -- | The type names used by a pattern. tnamesP :: Ord name => Pattern name -> Set name -- | The type names used by a match. tnamesM :: Ord name => Match name -> Set name -- | The type names used by a type schema. tnamesS :: Ord name => Schema name -> Set name -- | The type names used by a prop. tnamesC :: Ord name => Prop name -> Set name -- | Compute the type synonyms/type variables used by a type. tnamesT :: Ord name => Type name -> Set name -- | The purpose of this module is to convert all patterns to variable -- patterns. It also eliminates pattern bindings by de-sugaring them into -- Bind. Furthermore, here we associate signatures and pragmas -- with the names to which they belong. module Cryptol.Parser.NoPat class RemovePatterns t -- | Eliminate all patterns in a program. removePatterns :: RemovePatterns t => t -> (t, [Error]) data Error MultipleSignatures :: PName -> [Located (Schema PName)] -> Error SignatureNoBind :: (Located PName) -> (Schema PName) -> Error PragmaNoBind :: (Located PName) -> Pragma -> Error MultipleFixities :: PName -> [Range] -> Error FixityNoBind :: (Located PName) -> Error MultipleDocs :: PName -> [Range] -> Error instance Control.DeepSeq.NFData Cryptol.Parser.NoPat.Error instance GHC.Generics.Generic Cryptol.Parser.NoPat.Error instance GHC.Show.Show Cryptol.Parser.NoPat.Error instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Program Cryptol.Parser.Name.PName) instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Expr Cryptol.Parser.Name.PName) instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName) instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName] instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error module Cryptol.ModuleSystem.Exports modExports :: Ord name => Module name -> ExportSpec name data ExportSpec name ExportSpec :: Set name -> Set name -> ExportSpec name [eTypes] :: ExportSpec name -> Set name [eBinds] :: ExportSpec name -> Set name -- | Add a binding name to the export list, if it should be exported. exportBind :: Ord name => TopLevel name -> ExportSpec name -- | Add a type synonym name to the export list, if it should be exported. exportType :: Ord name => TopLevel name -> ExportSpec name -- | Check to see if a binding is exported. isExportedBind :: Ord name => name -> ExportSpec name -> Bool -- | Check to see if a type synonym is exported. isExportedType :: Ord name => name -> ExportSpec name -> Bool instance GHC.Generics.Generic (Cryptol.ModuleSystem.Exports.ExportSpec name) instance GHC.Show.Show name => GHC.Show.Show (Cryptol.ModuleSystem.Exports.ExportSpec name) instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.ModuleSystem.Exports.ExportSpec name) instance GHC.Classes.Ord name => GHC.Base.Semigroup (Cryptol.ModuleSystem.Exports.ExportSpec name) instance GHC.Classes.Ord name => GHC.Base.Monoid (Cryptol.ModuleSystem.Exports.ExportSpec name) module Cryptol.TypeCheck.AST data DeclDef DPrim :: DeclDef DExpr :: Expr -> DeclDef data Decl Decl :: !Name -> Schema -> DeclDef -> [Pragma] -> !Bool -> Maybe Fixity -> Maybe String -> Decl [dName] :: Decl -> !Name [dSignature] :: Decl -> Schema [dDefinition] :: Decl -> DeclDef [dPragmas] :: Decl -> [Pragma] [dInfix] :: Decl -> !Bool [dFixity] :: Decl -> Maybe Fixity [dDoc] :: Decl -> Maybe String data DeclGroup -- | Mutually recursive declarations Recursive :: [Decl] -> DeclGroup -- | Non-recursive declaration NonRecursive :: Decl -> DeclGroup data Match -- | Type arguments are the length and element type of the sequence -- expression From :: Name -> Type -> Type -> Expr -> Match Let :: Decl -> Match data Expr -- | List value (with type of elements) EList :: [Expr] -> Type -> Expr -- | Tuple value ETuple :: [Expr] -> Expr -- | Record value ERec :: [(Ident, Expr)] -> Expr -- | Elimination for tuplerecordlist ESel :: Expr -> Selector -> Expr -- | If-then-else EIf :: Expr -> Expr -> Expr -> Expr -- | List comprehensions The types cache the length of the sequence and its -- element type. EComp :: Type -> Type -> Expr -> [[Match]] -> Expr -- | Use of a bound variable EVar :: Name -> Expr -- | Function Value ETAbs :: TParam -> Expr -> Expr -- | Type application ETApp :: Expr -> Type -> Expr -- | Function application EApp :: Expr -> Expr -> Expr -- | Function value EAbs :: Name -> Type -> Expr -> Expr -- | Proof abstraction. Because we don't keep proofs around we don't need -- to name the assumption, but we still need to record the assumption. -- The assumption is the Type term, which should be of kind -- KProp. EProofAbs :: Prop -> Expr -> Expr -- | If `e : p => t`, then `EProofApp e : t`, as long as we can prove -- p. -- -- We don't record the actual proofs, as they are not used for anything. -- It may be nice to keep them around for sanity checking. EProofApp :: Expr -> Expr EWhere :: Expr -> [DeclGroup] -> Expr -- | A value parameter of a module. data ModVParam ModVParam :: Name -> Schema -> Maybe String -> Maybe Fixity -> ModVParam [mvpName] :: ModVParam -> Name [mvpType] :: ModVParam -> Schema [mvpDoc] :: ModVParam -> Maybe String [mvpFixity] :: ModVParam -> Maybe Fixity -- | A type parameter of a module. data ModTParam ModTParam :: Name -> Kind -> !Int -> Maybe String -> ModTParam [mtpName] :: ModTParam -> Name [mtpKind] :: ModTParam -> Kind -- | The number of the parameter in the module This is used when we move -- parameters from the module level to individual declarations (type -- synonyms in particular) [mtpNumber] :: ModTParam -> !Int [mtpDoc] :: ModTParam -> Maybe String -- | A Cryptol module. data Module Module :: !ModName -> ExportSpec Name -> [Import] -> Map Name TySyn -> Map Name Newtype -> Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> [DeclGroup] -> Module [mName] :: Module -> !ModName [mExports] :: Module -> ExportSpec Name [mImports] :: Module -> [Import] -- | This is just the type-level type synonyms of a module. [mTySyns] :: Module -> Map Name TySyn [mNewtypes] :: Module -> Map Name Newtype [mParamTypes] :: Module -> Map Name ModTParam [mParamConstraints] :: Module -> [Located Prop] [mParamFuns] :: Module -> Map Name ModVParam [mDecls] :: Module -> [DeclGroup] -- | Is this a parameterized module? isParametrizedModule :: Module -> Bool mtpParam :: ModTParam -> TParam groupDecls :: DeclGroup -> [Decl] -- | Construct a primitive, given a map to the unique names of the Cryptol -- module. ePrim :: PrimMap -> Ident -> Expr -- | Make an expression that is error pre-applied to a type and a -- message. eError :: PrimMap -> Type -> String -> Expr eString :: PrimMap -> String -> Expr eChar :: PrimMap -> Char -> Expr ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) splitAbs :: Expr -> Maybe ((Name, Type), Expr) splitTAbs :: Expr -> Maybe (TParam, Expr) splitProofAbs :: Expr -> Maybe (Prop, Expr) splitTApp :: Expr -> Maybe (Type, Expr) splitProofApp :: Expr -> Maybe ((), Expr) -- | Deconstruct an expression, typically polymorphic, into the types and -- proofs to which it is applied. Since we don't store the proofs, we -- just return the number of proof applications. The first type is the -- one closest to the expr. splitExprInst :: Expr -> (Expr, [Type], Int) data Name -- | Built-in type functions. If you add additional user-visible -- constructors, please update primTys in -- Cryptol.Prims.Types. data TFun -- | 
--   : Num -> Num -> Num
--
TCAdd :: TFun -- | 
--   : Num -> Num -> Num
--
TCSub :: TFun -- | 
--   : Num -> Num -> Num
--
TCMul :: TFun -- | 
--   : Num -> Num -> Num
--
TCDiv :: TFun -- | 
--   : Num -> Num -> Num
--
TCMod :: TFun -- | 
--   : Num -> Num -> Num
--
TCExp :: TFun -- | 
--   : Num -> Num
--
TCWidth :: TFun -- | 
--   : Num -> Num -> Num
--
TCMin :: TFun -- | 
--   : Num -> Num -> Num
--
TCMax :: TFun -- | 
--   : Num -> Num -> Num
--
TCCeilDiv :: TFun -- | 
--   : Num -> Num -> Num
--
TCCeilMod :: TFun -- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. ] -- :: [lengthFromThen 1 5 b][b] TCLenFromThen :: TFun -- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9 -- ] :: [lengthFromThenTo 1 5 9][b] TCLenFromThenTo :: TFun -- | Selectors are used for projecting from various components. Each -- selector has an option spec to specify the shape of the thing that is -- being selected. Currently, there is no surface syntax for list -- selectors, but they are used during the desugaring of patterns. data Selector -- | Zero-based tuple selection. Optionally specifies the shape of the -- tuple (one-based). TupleSel :: Int -> (Maybe Int) -> Selector -- | Record selection. Optionally specifies the shape of the record. RecordSel :: Ident -> (Maybe [Ident]) -> Selector -- | List selection. Optionally specifies the length of the list. ListSel :: Int -> (Maybe Int) -> Selector -- | An import declaration. data Import Import :: !ModName -> Maybe ModName -> Maybe ImportSpec -> Import [iModule] :: Import -> !ModName [iAs] :: Import -> Maybe ModName [iSpec] :: Import -> Maybe ImportSpec -- | The list of names following an import. -- -- INVARIANT: All of the Name entries in the list are expected -- to be unqualified names; the QName or NewName -- constructors should not be present. data ImportSpec Hiding :: [Ident] -> ImportSpec Only :: [Ident] -> ImportSpec -- | Export information for a declaration. data ExportType Public :: ExportType Private :: ExportType data ExportSpec name ExportSpec :: Set name -> Set name -> ExportSpec name [eTypes] :: ExportSpec name -> Set name [eBinds] :: ExportSpec name -> Set name -- | Check to see if a binding is exported. isExportedBind :: Ord name => name -> ExportSpec name -> Bool -- | Check to see if a type synonym is exported. isExportedType :: Ord name => name -> ExportSpec name -> Bool data Pragma PragmaNote :: String -> Pragma PragmaProperty :: Pragma data Fixity Fixity :: !Assoc -> !Int -> Fixity [fAssoc] :: Fixity -> !Assoc [fLevel] :: Fixity -> !Int -- | A mapping from an identifier defined in some module to its real name. data PrimMap PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap [primDecls] :: PrimMap -> Map Ident Name [primTypes] :: PrimMap -> Map Ident Name data TCErrorMessage TCErrorMessage :: !String -> TCErrorMessage [tcErrorMessage] :: TCErrorMessage -> !String instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Module instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Module instance GHC.Show.Show Cryptol.TypeCheck.AST.Module instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Match instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Match instance GHC.Show.Show Cryptol.TypeCheck.AST.Match instance GHC.Show.Show Cryptol.TypeCheck.AST.Decl instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Decl instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Decl instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclGroup instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclGroup instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclGroup instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Expr instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Expr instance GHC.Show.Show Cryptol.TypeCheck.AST.Expr instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclDef instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclDef instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclDef instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.ModVParam instance GHC.Generics.Generic Cryptol.TypeCheck.AST.ModVParam instance GHC.Show.Show Cryptol.TypeCheck.AST.ModVParam instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.ModTParam instance GHC.Generics.Generic Cryptol.TypeCheck.AST.ModTParam instance GHC.Show.Show Cryptol.TypeCheck.AST.ModTParam instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Module instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Module) instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Expr) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Expr instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Match) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Match instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclGroup) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Decl) instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclDef) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Decl module Cryptol.TypeCheck.TypeMap data TypeMap a TM :: Map TVar a -> Map TCon (List TypeMap a) -> Map [Ident] (List TypeMap a) -> TypeMap a [tvar] :: TypeMap a -> Map TVar a [tcon] :: TypeMap a -> Map TCon (List TypeMap a) [trec] :: TypeMap a -> Map [Ident] (List TypeMap a) type TypesMap = List TypeMap class TrieMap m k | m -> k emptyTM :: TrieMap m k => m a nullTM :: TrieMap m k => m a -> Bool lookupTM :: TrieMap m k => k -> m a -> Maybe a alterTM :: TrieMap m k => k -> (Maybe a -> Maybe a) -> m a -> m a unionTM :: TrieMap m k => (a -> a -> a) -> m a -> m a -> m a toListTM :: TrieMap m k => m a -> [(k, a)] mapMaybeWithKeyTM :: TrieMap m k => (k -> a -> Maybe b) -> m a -> m b insertTM :: TrieMap m k => k -> a -> m a -> m a insertWithTM :: TrieMap m k => (a -> a -> a) -> k -> a -> m a -> m a membersTM :: TrieMap m k => m a -> [a] mapTM :: TrieMap m k => (a -> b) -> m a -> m b mapWithKeyTM :: TrieMap m k => (k -> a -> b) -> m a -> m b mapMaybeTM :: TrieMap m k => (a -> Maybe b) -> m a -> m b data List m a L :: Maybe a -> m (List m a) -> List m a [nil] :: List m a -> Maybe a [cons] :: List m a -> m (List m a) instance GHC.Base.Functor Cryptol.TypeCheck.TypeMap.TypeMap instance GHC.Base.Functor m => GHC.Base.Functor (Cryptol.TypeCheck.TypeMap.List m) instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.TypeCheck.TypeMap.TypeMap Cryptol.TypeCheck.Type.Type instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.TypeMap.TypeMap a) instance Cryptol.TypeCheck.TypeMap.TrieMap m a => Cryptol.TypeCheck.TypeMap.TrieMap (Cryptol.TypeCheck.TypeMap.List m) [a] instance GHC.Classes.Ord a => Cryptol.TypeCheck.TypeMap.TrieMap (Data.Map.Internal.Map a) a -- | An interval interpretation of types. module Cryptol.TypeCheck.Solver.Numeric.Interval -- | Only meaningful for numeric types typeInterval :: Map TVar Interval -> Type -> Interval tvarInterval :: Map TVar Interval -> TVar -> Interval data IntervalUpdate NoChange :: IntervalUpdate InvalidInterval :: TVar -> IntervalUpdate NewIntervals :: (Map TVar Interval) -> IntervalUpdate updateInterval :: (TVar, Interval) -> Map TVar Interval -> IntervalUpdate computePropIntervals :: Map TVar Interval -> [Prop] -> IntervalUpdate -- | What we learn about variables from a single prop. propInterval :: Map TVar Interval -> Prop -> [(TVar, Interval)] data Interval Interval :: Nat' -> Maybe Nat' -> Interval -- | lower bound (inclusive) [iLower] :: Interval -> Nat' -- | upper bound (inclusive) If there is no upper bound, than all *natural* -- numbers. [iUpper] :: Interval -> Maybe Nat' ppIntervals :: Map TVar Interval -> Doc ppInterval :: Interval -> Doc iIsExact :: Interval -> Maybe Nat' iIsFin :: Interval -> Bool -- | Finite positive number. [1 .. inf). iIsPosFin :: Interval -> Bool -- | Returns True when the intervals definitely overlap, and -- False otherwise. iOverlap :: Interval -> Interval -> Bool -- | Intersect two intervals, yielding a new one that describes the space -- where they overlap. If the two intervals are disjoint, the result will -- be Nothing. iIntersect :: Interval -> Interval -> Maybe Interval -- | Any value iAny :: Interval -- | Any finite value iAnyFin :: Interval -- | Exactly this value iConst :: Nat' -> Interval iAdd :: Interval -> Interval -> Interval iMul :: Interval -> Interval -> Interval iExp :: Interval -> Interval -> Interval iMin :: Interval -> Interval -> Interval iMax :: Interval -> Interval -> Interval iSub :: Interval -> Interval -> Interval iDiv :: Interval -> Interval -> Interval iMod :: Interval -> Interval -> Interval iWidth :: Interval -> Interval iLenFromThen :: Interval -> Interval -> Interval -> Interval iLenFromThenTo :: Interval -> Interval -> Interval -> Interval instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.Interval.IntervalUpdate instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.Interval.Interval instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.Interval.Interval module Cryptol.TypeCheck.Solver.Types type Ctxt = Map TVar Interval data Solved -- | Solved, assuming the sub-goals. SolvedIf :: [Prop] -> Solved -- | We could not solve the goal. Unsolved :: Solved -- | The goal can never be solved. Unsolvable :: TCErrorMessage -> Solved elseTry :: Solved -> Solved -> Solved solveOpts :: [Solved] -> Solved matchThen :: Maybe a -> (a -> Solved) -> Solved guarded :: Bool -> Solved -> Solved instance GHC.Show.Show Cryptol.TypeCheck.Solver.Types.Solved instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Solver.Types.Solved -- | Simplification of fin constraints. module Cryptol.TypeCheck.Solver.Numeric.Fin cryIsFin :: Map TVar Interval -> Prop -> Solved cryIsFinType :: Map TVar Interval -> Type -> Solved module Cryptol.TypeCheck.Parseable class ShowParseable t showParseable :: ShowParseable t => t -> Doc maybeNameDoc :: Maybe Name -> Doc class ShowParseable t showParseable :: ShowParseable t => t -> Doc instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Expr instance (Cryptol.TypeCheck.Parseable.ShowParseable a, Cryptol.TypeCheck.Parseable.ShowParseable b) => Cryptol.TypeCheck.Parseable.ShowParseable (a, b) instance Cryptol.TypeCheck.Parseable.ShowParseable GHC.Types.Int instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.Utils.Ident.Ident instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.Type.Type instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.Parser.Selector.Selector instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Match instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Decl instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.DeclDef instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable [a] instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable (GHC.Base.Maybe a) instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable (Cryptol.Parser.Position.Located a) instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.Type.TParam instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.ModuleSystem.Name.Name -- | This module implements a transformation, which tries to avoid -- exponential slow down in some cases. What's the problem? Consider the -- following (common) patterns: -- -- fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ] -- -- The type of fibs is: -- -- {a} (a >= 1, fin a) => [inf][a] -- -- Here a is the number of bits to be used in the values -- computed by fibs. When we evaluate fibs, a -- becomes a parameter to fibs, which works except that now -- fibs is a function, and we don't get any of the memoization -- we might expect! What looked like an efficient implementation has all -- of a sudden become exponential! -- -- Note that this is only a problem for polymorphic values: if -- fibs was already a function, it would not be that surprising -- that it does not get cached. -- -- So, to avoid this, we try to spot recursive polymorphic values, where -- the recursive occurrences have the exact same type parameters as the -- definition. For example, this is the case in fibs: each -- recursive call to fibs is instantiated with exactly the same -- type parameter (i.e., a). The rewrite we do is as follows: -- -- fibs : {a} (a >= 1, fin a) => [inf][a] fibs = {a} (a >= 1, -- fin a) -> fibs' where fibs' : [inf][a] fibs' = [0,1] # [ x + y | x -- <- fibs', y <- drop`{1} fibs' ] -- -- After the rewrite, the recursion is monomorphic (i.e., we are always -- using the same type). As a result, fibs' is an ordinary -- recursive value, where we get the benefit of caching. -- -- The rewrite is a bit more complex, when there are multiple mutually -- recursive functions. Here is an example: -- -- zig : {a} (a >= 2, fin a) => [inf][a] zig = [1] # zag -- -- zag : {a} (a >= 2, fin a) => [inf][a] zag = [2] # zig -- -- This gets rewritten to: -- -- newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a]) newName = -- {a} (a >= 2, fin a) -> (zig', zag') where zig' : [inf][a] zig' = -- [1] # zag' -- -- zag' : [inf][a] zag' = [2] # zig' -- -- zig : {a} (a >= 2, fin a) => [inf][a] zig = {a} (a >= 2, fin -- a) -> (newName a <> <> ).1 -- -- zag : {a} (a >= 2, fin a) => [inf][a] zag = {a} (a >= 2, fin -- a) -> (newName a <> <> ).2 -- -- NOTE: We are assuming that no capture would occur with binders. For -- values, this is because we replaces things with freshly chosen -- variables. For types, this should be because there should be no -- shadowing in the types. XXX: Make sure that this really is the case -- for types!! module Cryptol.Transform.MonoValues -- | Note that this assumes that this pass will be run only once for each -- module, otherwise we will get name collisions. rewModule :: Supply -> Module -> (Module, Supply) instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.Transform.MonoValues.RewMap' (Cryptol.ModuleSystem.Name.Name, [Cryptol.TypeCheck.Type.Type], GHC.Types.Int) -- | Transformed a parametrized module into an ordinary module where -- everything is parameterized by the module's parameters. Note that this -- reuses the names from the original parameterized module. module Cryptol.Transform.AddModParams addModParams :: Module -> Either [Name] Module instance Cryptol.Transform.AddModParams.Inst a => Cryptol.Transform.AddModParams.Inst [a] instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Expr instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Match instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Decl instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.DeclDef instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.Type instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.TySyn instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.Newtype instance Cryptol.Transform.AddModParams.AddParams a => Cryptol.Transform.AddModParams.AddParams [a] instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Schema instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Type instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.Expr instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.Decl instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.TySyn instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Newtype module Cryptol.IR.FreeVars class FreeVars e freeVars :: FreeVars e => e -> Deps data Deps Deps :: Set Name -> Set Name -> Set TParam -> Deps -- | Undefined value names [valDeps] :: Deps -> Set Name -- | Undefined type names (from newtype) [tyDeps] :: Deps -> Set Name -- | Undefined type params (e.d. mod params) [tyParams] :: Deps -> Set TParam class Defs d defs :: Defs d => d -> Set Name -- | Dependencies of top-level declarations in a module. These are -- dependencies on module parameters or things defined outside the -- module. moduleDeps :: Module -> Map Name Deps -- | Compute the transitive closure of the given dependencies. transDeps :: Map Name Deps -> Map Name Deps instance GHC.Classes.Eq Cryptol.IR.FreeVars.Deps instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Expr instance Cryptol.IR.FreeVars.Defs a => Cryptol.IR.FreeVars.Defs [a] instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.Decl instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.Match instance Cryptol.IR.FreeVars.FreeVars e => Cryptol.IR.FreeVars.FreeVars [e] instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Decl instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.DeclDef instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Match instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Schema instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Type instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.TVar instance Cryptol.IR.FreeVars.FreeVars Cryptol.Prims.Syntax.TCon instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Newtype instance GHC.Base.Semigroup Cryptol.IR.FreeVars.Deps instance GHC.Base.Monoid Cryptol.IR.FreeVars.Deps -- | Utility functions that are also useful for translating programs from -- previous Cryptol versions. module Cryptol.Parser.Utils translateExprToNumT :: Expr PName -> Maybe (Type PName) widthIdent :: Ident module Cryptol.ModuleSystem.Interface -- | The resulting interface generated by a module that has been -- typechecked. data Iface Iface :: !ModName -> IfaceDecls -> IfaceDecls -> IfaceParams -> Iface -- | Module name [ifModName] :: Iface -> !ModName -- | Exported definitions [ifPublic] :: Iface -> IfaceDecls -- | Private defintiions [ifPrivate] :: Iface -> IfaceDecls -- | Uninterpreted constants (aka module params) [ifParams] :: Iface -> IfaceParams data IfaceDecls IfaceDecls :: Map Name IfaceTySyn -> Map Name IfaceNewtype -> Map Name IfaceDecl -> IfaceDecls [ifTySyns] :: IfaceDecls -> Map Name IfaceTySyn [ifNewtypes] :: IfaceDecls -> Map Name IfaceNewtype [ifDecls] :: IfaceDecls -> Map Name IfaceDecl type IfaceTySyn = TySyn ifTySynName :: TySyn -> Name type IfaceNewtype = Newtype data IfaceDecl IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl -- | Name of thing [ifDeclName] :: IfaceDecl -> !Name -- | Type [ifDeclSig] :: IfaceDecl -> Schema -- | Pragmas [ifDeclPragmas] :: IfaceDecl -> [Pragma] -- | Is this an infix thing [ifDeclInfix] :: IfaceDecl -> Bool -- | Fixity information [ifDeclFixity] :: IfaceDecl -> Maybe Fixity -- | Documentation [ifDeclDoc] :: IfaceDecl -> Maybe String mkIfaceDecl :: Decl -> IfaceDecl data IfaceParams IfaceParams :: Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> IfaceParams [ifParamTypes] :: IfaceParams -> Map Name ModTParam -- | Constraints on param. types [ifParamConstraints] :: IfaceParams -> [Located Prop] [ifParamFuns] :: IfaceParams -> Map Name ModVParam -- | Generate an Iface from a typechecked module. genIface :: Module -> Iface -- | Produce a PrimMap from an interface. -- -- NOTE: the map will expose both public and private names. ifacePrimMap :: Iface -> PrimMap noIfaceParams :: IfaceParams instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.Iface instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.Iface instance GHC.Show.Show Cryptol.ModuleSystem.Interface.Iface instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecls instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecls instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecls instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecl instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecl instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecl instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceParams instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceParams instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceParams instance GHC.Base.Semigroup Cryptol.ModuleSystem.Interface.IfaceDecls instance GHC.Base.Monoid Cryptol.ModuleSystem.Interface.IfaceDecls module Cryptol.ModuleSystem.NamingEnv data NamingEnv NamingEnv :: !(Map PName [Name]) -> !(Map PName [Name]) -> !(Map Name Fixity) -> NamingEnv -- | Expr renaming environment [neExprs] :: NamingEnv -> !(Map PName [Name]) -- | Type renaming environment [neTypes] :: NamingEnv -> !(Map PName [Name]) -- | Expression-level fixity environment [neFixity] :: NamingEnv -> !(Map Name Fixity) -- | Return a list of value-level names to which this parsed name may -- refer. lookupValNames :: PName -> NamingEnv -> [Name] -- | Return a list of type-level names to which this parsed name may refer. lookupTypeNames :: PName -> NamingEnv -> [Name] -- | Merge two name maps, collapsing cases where the entries are the same, -- and producing conflicts otherwise. merge :: [Name] -> [Name] -> [Name] -- | Generate a mapping from Ident to Name for a given naming -- environment. toPrimMap :: NamingEnv -> PrimMap -- | Generate a display format based on a naming environment. toNameDisp :: NamingEnv -> NameDisp -- | Produce sets of visible names for types and declarations. -- -- NOTE: if entries in the NamingEnv would have produced a name clash, -- they will be omitted from the resulting sets. visibleNames :: NamingEnv -> (Set Name, Set Name) -- | Qualify all symbols in a NamingEnv with the given prefix. qualify :: ModName -> NamingEnv -> NamingEnv filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv -- | Singleton type renaming environment. singletonT :: PName -> Name -> NamingEnv -- | Singleton expression renaming environment. singletonE :: PName -> Name -> NamingEnv -- | Like mappend, but when merging, prefer values on the lhs. shadowing :: NamingEnv -> NamingEnv -> NamingEnv travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv data InModule a InModule :: !ModName -> a -> InModule a -- | Generate a NamingEnv using an explicit supply. namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply) newTop :: FreshM m => ModName -> PName -> Maybe Fixity -> Range -> m Name newLocal :: FreshM m => PName -> Range -> m Name newtype BuildNamingEnv BuildNamingEnv :: SupplyT Id NamingEnv -> BuildNamingEnv [runBuild] :: BuildNamingEnv -> SupplyT Id NamingEnv -- | Things that define exported names. class BindsNames a namingEnv :: BindsNames a => a -> BuildNamingEnv -- | Interpret an import in the context of an interface, to produce a name -- environment for the renamer, and a NameDisp for -- pretty-printing. interpImport :: Import -> IfaceDecls -> NamingEnv -- | Generate a naming environment from a declaration interface, where none -- of the names are qualified. unqualifiedEnv :: IfaceDecls -> NamingEnv -- | Compute an unqualified naming environment, containing the various -- module parameters. modParamsNamingEnv :: IfaceParams -> NamingEnv data ImportIface ImportIface :: Import -> Iface -> ImportIface instance GHC.Show.Show a => GHC.Show.Show (Cryptol.ModuleSystem.NamingEnv.InModule a) instance Data.Foldable.Foldable Cryptol.ModuleSystem.NamingEnv.InModule instance Data.Traversable.Traversable Cryptol.ModuleSystem.NamingEnv.InModule instance GHC.Base.Functor Cryptol.ModuleSystem.NamingEnv.InModule instance Control.DeepSeq.NFData Cryptol.ModuleSystem.NamingEnv.NamingEnv instance GHC.Generics.Generic Cryptol.ModuleSystem.NamingEnv.NamingEnv instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NamingEnv instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.ImportIface instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.NamingEnv instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames (GHC.Base.Maybe a) instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames [a] instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Schema Cryptol.Parser.Name.PName) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Bind Cryptol.Parser.Name.PName)) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.TParam Cryptol.Parser.Name.PName) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.TopDecl Cryptol.Parser.Name.PName)) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.ParameterFun Cryptol.Parser.Name.PName)) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.ParameterType Cryptol.Parser.Name.PName)) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Newtype Cryptol.Parser.Name.PName)) instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName)) instance GHC.Base.Semigroup Cryptol.ModuleSystem.NamingEnv.BuildNamingEnv instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.BuildNamingEnv instance GHC.Base.Semigroup Cryptol.ModuleSystem.NamingEnv.NamingEnv instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.NamingEnv module Cryptol.ModuleSystem.Renamer data NamingEnv -- | Like mappend, but when merging, prefer values on the lhs. shadowing :: NamingEnv -> NamingEnv -> NamingEnv -- | Things that define exported names. class BindsNames a namingEnv :: BindsNames a => a -> BuildNamingEnv data InModule a InModule :: !ModName -> a -> InModule a -- | Generate a NamingEnv using an explicit supply. namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply) -- | Throw errors for any names that overlap in a rewrite environment. checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning]) -- | Shadow the current naming environment with some more names. shadowNames :: BindsNames env => env -> RenameM a -> RenameM a class Rename f rename :: Rename f => f PName -> RenameM (f Name) runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a -> (Either [RenamerError] (a, Supply), [RenamerWarning]) data RenameM a data RenamerError -- | Multiple imported symbols contain this name MultipleSyms :: (Located PName) -> [Name] -> NameDisp -> RenamerError -- | Expression name is not bound to any definition UnboundExpr :: (Located PName) -> NameDisp -> RenamerError -- | Type name is not bound to any definition UnboundType :: (Located PName) -> NameDisp -> RenamerError -- | An environment has produced multiple overlapping symbols OverlappingSyms :: [Name] -> NameDisp -> RenamerError -- | When a value is expected from the naming environment, but one or more -- types exist instead. ExpectedValue :: (Located PName) -> NameDisp -> RenamerError -- | When a type is missing from the naming environment, but one or more -- values exist with the same name. ExpectedType :: (Located PName) -> NameDisp -> RenamerError -- | When the fixity of two operators conflict FixityError :: (Located Name) -> (Located Name) -> NameDisp -> RenamerError -- | When it's not possible to produce a Prop from a Type. InvalidConstraint :: (Type PName) -> NameDisp -> RenamerError -- | When a builtin type/type-function is used incorrectly. MalformedBuiltin :: (Type PName) -> PName -> NameDisp -> RenamerError -- | When a builtin type is named in a binder. BoundReservedType :: PName -> (Maybe Range) -> Doc -> NameDisp -> RenamerError data RenamerWarning SymbolShadowed :: Name -> [Name] -> NameDisp -> RenamerWarning DangerousFixity :: (Located Name) -> (Located Name) -> NameDisp -> RenamerWarning UnusedName :: Name -> NameDisp -> RenamerWarning renameVar :: PName -> RenameM Name renameType :: PName -> RenameM Name renameModule :: Module PName -> RenameM (NamingEnv, Module Name) instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.EnvCheck instance GHC.Classes.Eq Cryptol.ModuleSystem.Renamer.EnvCheck instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerWarning instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerWarning instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerWarning instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerError instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerError instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerError instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TopDecl instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.ParameterType instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.ParameterFun instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Decl instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Newtype instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Schema instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TParam instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Prop instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Type instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Bind instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.BindDef instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pattern instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Expr instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TypeInst instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Match instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TySyn instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.PropSyn instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Cryptol.ModuleSystem.Renamer.RenameM a) instance (GHC.Base.Semigroup a, GHC.Base.Monoid a) => GHC.Base.Monoid (Cryptol.ModuleSystem.Renamer.RenameM a) instance GHC.Base.Functor Cryptol.ModuleSystem.Renamer.RenameM instance GHC.Base.Applicative Cryptol.ModuleSystem.Renamer.RenameM instance GHC.Base.Monad Cryptol.ModuleSystem.Renamer.RenameM instance Cryptol.ModuleSystem.Name.FreshM Cryptol.ModuleSystem.Renamer.RenameM instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerWarning instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerError module Cryptol.Eval.Monad -- | The monad for Cryptol evaluation. data Eval a Ready :: !a -> Eval a Thunk :: !(EvalOpts -> IO a) -> Eval a -- | Execute the given evaluation action. runEval :: EvalOpts -> Eval a -> IO a -- | Some options for evalutaion data EvalOpts EvalOpts :: Logger -> PPOpts -> EvalOpts -- | Where to print stuff (e.g., for trace) [evalLogger] :: EvalOpts -> Logger -- | How to pretty print things. [evalPPOpts] :: EvalOpts -> PPOpts -- | Access the evaluation options. getEvalOpts :: Eval EvalOpts -- | How to pretty print things when evaluating data PPOpts PPOpts :: Bool -> Int -> Int -> PPOpts [useAscii] :: PPOpts -> Bool [useBase] :: PPOpts -> Int [useInfLength] :: PPOpts -> Int -- | Lift an IO computation into the Eval monad. io :: IO a -> Eval a -- | Delay the given evaluation computation, returning a thunk which will -- run the computation when forced. Raise a loop error if the resulting -- thunk is forced during its own evaluation. delay :: Maybe String -> Eval a -> Eval (Eval a) -- | Delay the given evaluation computation, returning a thunk which will -- run the computation when forced. Run the retry computation -- instead if the resulting thunk is forced during its own evaluation. delayFill :: Eval a -> Eval a -> Eval (Eval a) -- | A computation that returns an already-evaluated value. ready :: a -> Eval a -- | Produce a thunk value which can be filled with its associated -- computation after the fact. A preallocated thunk is returned, along -- with an operation to fill the thunk with the associated computation. -- This is used to implement recursive declaration groups. blackhole :: String -> Eval (Eval a, Eval a -> Eval ()) -- | Data type describing errors that can occur during evaluation. data EvalError -- | Out-of-bounds index InvalidIndex :: Integer -> EvalError -- | Non-numeric type passed to number function TypeCannotBeDemoted :: Type -> EvalError -- | Division or modulus by 0 DivideByZero :: EvalError -- | Exponentiation by negative integer NegativeExponent :: EvalError -- | Logarithm of a negative integer LogNegative :: EvalError -- | Bitvector too large WordTooWide :: Integer -> EvalError -- | Call to the Cryptol error primitive UserError :: String -> EvalError -- | Detectable nontermination LoopError :: String -> EvalError -- | Panic from an Eval context. evalPanic :: HasCallStack => String -> [String] -> a -- | For things like `(inf) or `(0-1). typeCannotBeDemoted :: Type -> a -- | For division by 0. divideByZero :: Eval a -- | For exponentiation by a negative integer. negativeExponent :: Eval a -- | For logarithm of a negative integer. logNegative :: Eval a -- | For when we know that a word is too wide and will exceed gmp's limits -- (though words approaching this size will probably cause the system to -- crash anyway due to lack of memory). wordTooWide :: Integer -> a -- | For the Cryptol error function. cryUserError :: String -> Eval a -- | For cases where we can detect tight loops. cryLoopError :: String -> Eval a -- | A sequencing operation has gotten an invalid index. invalidIndex :: Integer -> Eval a instance GHC.Show.Show Cryptol.Eval.Monad.EvalError instance Cryptol.Utils.PP.PP Cryptol.Eval.Monad.EvalError instance GHC.Exception.Exception Cryptol.Eval.Monad.EvalError instance GHC.Base.Functor Cryptol.Eval.Monad.Eval instance GHC.Base.Applicative Cryptol.Eval.Monad.Eval instance GHC.Base.Monad Cryptol.Eval.Monad.Eval instance Control.Monad.IO.Class.MonadIO Cryptol.Eval.Monad.Eval instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Eval.Monad.Eval a) instance Control.Monad.Fix.MonadFix Cryptol.Eval.Monad.Eval module Cryptol.Eval.Type -- | An evaluated type of kind *. These types do not contain type -- variables, type synonyms, or type functions. data TValue -- | 
--   Bit
--
TVBit :: TValue -- | 
--   Integer
--
TVInteger :: TValue -- | 
--   Z n
--
TVIntMod :: Integer -> TValue -- | 
--   [n]a
--
TVSeq :: Integer -> TValue -> TValue -- | 
--   [inf]t
--
TVStream :: TValue -> TValue -- | 
--   (a, b, c )
--
TVTuple :: [TValue] -> TValue -- | 
--   { x : a, y : b, z : c }
--
TVRec :: [(Ident, TValue)] -> TValue -- | 
--   a -> b
--
TVFun :: TValue -> TValue -> TValue -- | Convert a type value back into a regular type tValTy :: TValue -> Type -- | True if the evaluated value is Bit isTBit :: TValue -> Bool -- | Produce a sequence type value tvSeq :: Nat' -> TValue -> TValue -- | Coerce an extended natural into an integer, for values known to be -- finite finNat' :: Nat' -> Integer type TypeEnv = Map TVar (Either Nat' TValue) -- | Evaluation for types (kind * or #). evalType :: HasCallStack => TypeEnv -> Type -> Either Nat' TValue -- | Evaluation for value types (kind *). evalValType :: HasCallStack => TypeEnv -> Type -> TValue -- | Evaluation for number types (kind #). evalNumType :: HasCallStack => TypeEnv -> Type -> Nat' -- | Reduce type functions, raising an exception for undefined values. evalTF :: HasCallStack => TFun -> [Nat'] -> Nat' instance Control.DeepSeq.NFData Cryptol.Eval.Type.TValue instance GHC.Generics.Generic Cryptol.Eval.Type.TValue instance GHC.Show.Show Cryptol.Eval.Type.TValue module Cryptol.Eval.Value -- | Concrete bitvector values: width, value Invariant: The value must be -- within the range 0 .. 2^width-1 data BV BV :: !Integer -> !Integer -> BV -- | Apply an integer function to the values of bitvectors. This function -- assumes both bitvectors are the same width. binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV -- | Apply an integer function to the values of a bitvector. This function -- assumes the function will not require masking. unaryBV :: (Integer -> Integer) -> BV -> BV bvVal :: BV -> Integer -- | Smart constructor for BVs that checks for the width limit mkBv :: Integer -> Integer -> BV -- | A sequence map represents a mapping from nonnegative integer indices -- to values. These are used to represent both finite and infinite -- sequences. data SeqMap b w i IndexSeqMap :: !(Integer -> Eval (GenValue b w i)) -> SeqMap b w i UpdateSeqMap :: !(Map Integer (Eval (GenValue b w i))) -> !(Integer -> Eval (GenValue b w i)) -> SeqMap b w i lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) type SeqValMap = SeqMap Bool BV Integer -- | Generate a finite sequence map from a list of values finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i -- | Generate an infinite sequence map from a stream of values infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i) -- | Create a finite list of length n of the values from [0..n-1] -- in the given the sequence emap. enumerateSeqMap :: (Integral n) => n -> SeqMap b w i -> [Eval (GenValue b w i)] -- | Create an infinite stream of all the values in a sequence map streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)] -- | Reverse the order of a finite sequence map reverseSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i -- | Concatenate the first n values of the first sequence map onto -- the beginning of the second sequence map. concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i -- | Given a number n and a sequence map, return two new sequence -- maps: the first containing the values from `[0..n-1]` and the next -- containing the values from n onward. splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i) -- | Drop the first n elements of the given SeqMap. dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -- | Given a sequence map, return a new sequence map that is memoized using -- a finite map memo table. memoMap :: SeqMap b w i -> Eval (SeqMap b w i) -- | Apply the given evaluation function pointwise to the two given -- sequence maps. zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> SeqMap b w i -> Eval (SeqMap b w i) -- | Apply the given function to each value in the given sequence map mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> Eval (SeqMap b w i) -- | For efficency reasons, we handle finite sequences of bits as special -- cases in the evaluator. In cases where we know it is safe to do so, we -- prefer to used a "packed word" representation of bit sequences. This -- allows us to rely directly on Integer types (in the concrete -- evalautor) and SBV's Word types (in the symbolic simulator). -- -- However, if we cannot be sure all the bits of the sequence will -- eventually be forced, we must instead rely on an explicit sequence of -- bits representation. data WordValue b w i -- | Packed word representation for bit sequences. WordVal :: !w -> WordValue b w i -- | Sequence of thunks representing bits. BitsVal :: !(Seq (Eval b)) -> WordValue b w i -- | A large bitvector sequence, represented as a SeqMap of bits. LargeBitsVal :: !Integer -> !(SeqMap b w i) -> WordValue b w i -- | An arbitrarily-chosen number of elements where we switch from a dense -- sequence representation of bit-level words to SeqMap -- representation. largeBitSize :: Integer -- | Force a word value into packed word form asWordVal :: BitWord b w i => WordValue b w i -> Eval w -- | Force a word value into a sequence of bits asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i -- | Turn a word value into a sequence of bits, forcing each bit. The -- sequence is returned in big-endian order. enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b] -- | Turn a word value into a sequence of bits, forcing each bit. The -- sequence is returned in reverse of the usual order, which is -- little-endian order. enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b] -- | Compute the size of a word value wordValueSize :: BitWord b w i => WordValue b w i -> Integer checkedSeqIndex :: Seq a -> Integer -> Eval a checkedIndex :: [a] -> Integer -> Eval a -- | Select an individual bit from a word value indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -- | Produce a new WordValue from the one given by updating the -- ith bit with the given bit value. updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i) -- | Generic value type, parameterized by bit and word types. -- -- NOTE: we maintain an important invariant regarding sequence types. -- VSeq must never be used for finite sequences of bits. Always -- use the VWord constructor instead! Infinite sequences of bits -- are handled by the VStream constructor, just as for other -- types. data GenValue b w i -- | 
--   { .. }
--
VRecord :: ![(Ident, Eval (GenValue b w i))] -> GenValue b w i -- | 
--   ( .. )
--
VTuple :: ![Eval (GenValue b w i)] -> GenValue b w i -- | 
--   Bit
--
VBit :: !b -> GenValue b w i -- | Integer or Z n VInteger :: !i -> GenValue b w i -- | [n]a Invariant: VSeq is never a sequence of bits VSeq :: !Integer -> !(SeqMap b w i) -> GenValue b w i -- | 
--   [n]Bit
--
VWord :: !Integer -> !(Eval (WordValue b w i)) -> GenValue b w i -- | 
--   [inf]a
--
VStream :: !(SeqMap b w i) -> GenValue b w i -- | functions VFun :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i -- | polymorphic values (kind *) VPoly :: (TValue -> Eval (GenValue b w i)) -> GenValue b w i -- | polymorphic values (kind #) VNumPoly :: (Nat' -> Eval (GenValue b w i)) -> GenValue b w i -- | Force the evaluation of a word value forceWordValue :: WordValue b w i -> Eval () -- | Force the evaluation of a value forceValue :: GenValue b w i -> Eval () type Value = GenValue Bool BV Integer defaultPPOpts :: PPOpts atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c) atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b) ppValue :: forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc asciiMode :: PPOpts -> Integer -> Bool integerToChar :: Integer -> Char ppBV :: PPOpts -> BV -> Doc -- | This type class defines a collection of operations on bits and words -- that are necessary to define generic evaluator primitives that operate -- on both concrete and symbolic values uniformly. class BitWord b w i | b -> w, w -> i, i -> b -- | Pretty-print an individual bit ppBit :: BitWord b w i => b -> Doc -- | Pretty-print a word value ppWord :: BitWord b w i => PPOpts -> w -> Doc -- | Pretty-print an integer value ppInteger :: BitWord b w i => PPOpts -> i -> Doc -- | Attempt to render a word value as an ASCII character. Return -- Nothing if the character value is unknown (e.g., for symbolic -- values). wordAsChar :: BitWord b w i => w -> Maybe Char -- | The number of bits in a word value. wordLen :: BitWord b w i => w -> Integer -- | Construct a literal bit value from a boolean. bitLit :: BitWord b w i => Bool -> b -- | Construct a literal word value given a bit width and a value. wordLit :: BitWord b w i => Integer -> Integer -> w -- | Construct a literal integer value from the given integer. integerLit :: BitWord b w i => Integer -> i -- | Extract the numbered bit from the word. -- -- NOTE: this assumes that the sequence of bits is big-endian and finite, -- so the bit numbered 0 is the most significant bit. wordBit :: BitWord b w i => w -> Integer -> b -- | Update the numbered bit in the word. -- -- NOTE: this assumes that the sequence of bits is big-endian and finite, -- so the bit numbered 0 is the most significant bit. wordUpdate :: BitWord b w i => w -> Integer -> b -> w -- | Construct a word value from a finite sequence of bits. NOTE: this -- assumes that the sequence of bits is big-endian and finite, so the -- first element of the list will be the most significant bit. packWord :: BitWord b w i => [b] -> w -- | Deconstruct a packed word value in to a finite sequence of bits. NOTE: -- this produces a list of bits that represent a big-endian word, so the -- most significant bit is the first element of the list. unpackWord :: BitWord b w i => w -> [b] -- | Concatenate the two given word values. NOTE: the first argument -- represents the more-significant bits joinWord :: BitWord b w i => w -> w -> w -- | Take the most-significant bits, and return those bits and the -- remainder. The first element of the pair is the most significant bits. -- The two integer sizes must sum to the length of the given word value. splitWord :: BitWord b w i => Integer -> Integer -> w -> (w, w) -- | Extract a subsequence of bits from a packed word value. The first -- integer argument is the number of bits in the resulting word. The -- second integer argument is the number of less-significant digits to -- discard. Stated another way, the operation `extractWord n i w` is -- equivalent to first shifting w right by i bits, and -- then truncating to n bits. extractWord :: BitWord b w i => Integer -> Integer -> w -> w -- | 2's complement addition of packed words. The arguments must have equal -- bit width, and the result is of the same width. Overflow is silently -- discarded. wordPlus :: BitWord b w i => w -> w -> w -- | 2's complement subtraction of packed words. The arguments must have -- equal bit width, and the result is of the same width. Overflow is -- silently discarded. wordMinus :: BitWord b w i => w -> w -> w -- | 2's complement multiplication of packed words. The arguments must have -- equal bit width, and the result is of the same width. The high bits of -- the multiplication are silently discarded. wordMult :: BitWord b w i => w -> w -> w -- | Construct an integer value from the given packed word. wordToInt :: BitWord b w i => w -> i -- | Addition of unbounded integers. intPlus :: BitWord b w i => i -> i -> i -- | Subtraction of unbounded integers. intMinus :: BitWord b w i => i -> i -> i -- | Multiplication of unbounded integers. intMult :: BitWord b w i => i -> i -> i -- | Addition of integers modulo n, for a concrete positive integer n. intModPlus :: BitWord b w i => Integer -> i -> i -> i -- | Subtraction of integers modulo n, for a concrete positive integer n. intModMinus :: BitWord b w i => Integer -> i -> i -> i -- | Multiplication of integers modulo n, for a concrete positive integer -- n. intModMult :: BitWord b w i => Integer -> i -> i -> i -- | Construct a packed word of the specified width from an integer value. wordFromInt :: BitWord b w i => Integer -> i -> w -- | This class defines additional operations necessary to define generic -- evaluation functions. class BitWord b w i => EvalPrims b w i -- | Eval prim binds primitive declarations to the primitive values that -- implement them. evalPrim :: EvalPrims b w i => Decl -> GenValue b w i -- | ifthenelse operation. Choose either the 'then' value or the -- 'else' value depending on the value of the test bit. iteValue :: EvalPrims b w i => b -> Eval (GenValue b w i) -> Eval (GenValue b w i) -> Eval (GenValue b w i) mask :: Integer -> Integer -> Integer -- | Create a packed word of n bits. word :: BitWord b w i => Integer -> Integer -> GenValue b w i lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i -- | Functions that assume word inputs wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i -- | A type lambda that expects a Type. tlam :: (TValue -> GenValue b w i) -> GenValue b w i -- | A type lambda that expects a Type of kind #. nlam :: (Nat' -> GenValue b w i) -> GenValue b w i -- | Generate a stream. toStream :: [GenValue b w i] -> Eval (GenValue b w i) toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i -- | This is strict! boolToWord :: [Bool] -> Value -- | Construct either a finite sequence, or a stream. In the finite case, -- record whether or not the elements were bits, to aid pretty-printing. toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i) -- | Construct either a finite sequence, or a stream. In the finite case, -- record whether or not the elements were bits, to aid pretty-printing. mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i -- | Extract a bit value. fromVBit :: GenValue b w i -> b -- | Extract an integer value. fromVInteger :: GenValue b w i -> i -- | Extract a finite sequence value. fromVSeq :: GenValue b w i -> SeqMap b w i -- | Extract a sequence. fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i) fromStr :: Value -> Eval String fromBit :: GenValue b w i -> Eval b fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i) -- | Extract a packed word. fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer -- | If the given list of values are all fully-evaluated thunks containing -- bits, return a packed word built from the same bits. However, if any -- value is not a fully-evaluated bit, return Nothing. tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w -- | Turn a value into an integer represented by w bits. fromWord :: String -> Value -> Eval Integer -- | Extract a function from a value. fromVFun :: GenValue b w i -> (Eval (GenValue b w i) -> Eval (GenValue b w i)) -- | Extract a polymorphic function from a value. fromVPoly :: GenValue b w i -> (TValue -> Eval (GenValue b w i)) -- | Extract a polymorphic function from a value. fromVNumPoly :: GenValue b w i -> (Nat' -> Eval (GenValue b w i)) -- | Extract a tuple from a value. fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)] -- | Extract a record from a value. fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))] -- | Lookup a field in a record. lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i) -- | Given an expected type, returns an expression that evaluates to this -- value, if we can determine it. -- -- XXX: View patterns would probably clean up this definition a lot. toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr) instance (Control.DeepSeq.NFData w, Control.DeepSeq.NFData b) => Control.DeepSeq.NFData (Cryptol.Eval.Value.WordValue b w i) instance GHC.Generics.Generic (Cryptol.Eval.Value.WordValue b w i) instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData i, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Value.GenValue b w i) instance GHC.Generics.Generic (Cryptol.Eval.Value.GenValue b w i) instance Control.DeepSeq.NFData Cryptol.Eval.Value.BV instance GHC.Generics.Generic Cryptol.Eval.Value.BV instance Cryptol.Eval.Value.BitWord GHC.Types.Bool Cryptol.Eval.Value.BV GHC.Integer.Type.Integer instance Control.DeepSeq.NFData (Cryptol.Eval.Value.SeqMap b w i) instance (GHC.Show.Show b, GHC.Show.Show w, GHC.Show.Show i) => GHC.Show.Show (Cryptol.Eval.Value.GenValue b w i) instance GHC.Show.Show Cryptol.Eval.Value.BV module Cryptol.Testing.Concrete -- | A test result is either a pass, a failure due to evaluating to -- False, or a failure due to an exception raised during -- evaluation data TestResult Pass :: TestResult FailFalse :: [Value] -> TestResult FailError :: EvalError -> [Value] -> TestResult isPass :: TestResult -> Bool -- | Apply a testable value to some arguments. Note that this function -- assumes that the values come from a call to testableType (i.e., -- things are type-correct). We run in the IO monad in order to catch any -- EvalErrors. runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult -- | Given a (function) type, compute all possible inputs for it. We also -- return the types of the arguments and the total number of test (i.e., -- the length of the outer list. testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]]) -- | Given a fully-evaluated type, try to compute the number of values in -- it. Returns Nothing for infinite types, user-defined types, -- polymorphic types, and, currently, function spaces. Of course, we can -- easily compute the sizes of function spaces, but we can't easily -- enumerate their inhabitants. typeSize :: Type -> Maybe Integer -- | Returns all the values in a type. Returns an empty list of values, for -- types where typeSize returned Nothing. typeValues :: Type -> [Value] data TestSpec m s TestSpec :: Integer -> s -> m (TestResult, s) -> String -> Integer -> Maybe Integer -> Integer -> Integer -> m () -> m () -> TestResult -> m () -> m () -> TestSpec m s [testFn] :: TestSpec m s -> Integer -> s -> m (TestResult, s) -- | The property as entered by the user [testProp] :: TestSpec m s -> String [testTotal] :: TestSpec m s -> Integer -- | Nothing indicates infinity [testPossible] :: TestSpec m s -> Maybe Integer [testRptProgress] :: TestSpec m s -> Integer -> Integer -> m () [testClrProgress] :: TestSpec m s -> m () [testRptFailure] :: TestSpec m s -> TestResult -> m () [testRptSuccess] :: TestSpec m s -> m () data TestReport TestReport :: TestResult -> String -> Integer -> Maybe Integer -> TestReport [reportResult] :: TestReport -> TestResult -- | The property as entered by the user [reportProp] :: TestReport -> String [reportTestsRun] :: TestReport -> Integer [reportTestsPossible] :: TestReport -> Maybe Integer runTests :: Monad m => TestSpec m s -> s -> m TestReport module Cryptol.Symbolic.Value type SBool = SVal type SWord = SVal type SInteger = SVal literalSWord :: Int -> Integer -> SWord fromBitsLE :: [SBool] -> SWord forallBV_ :: Int -> Symbolic SWord existsBV_ :: Int -> Symbolic SWord forallSBool_ :: Symbolic SBool existsSBool_ :: Symbolic SBool forallSInteger_ :: Symbolic SBool existsSInteger_ :: Symbolic SBool type Value = GenValue SBool SWord SInteger -- | An evaluated type of kind *. These types do not contain type -- variables, type synonyms, or type functions. data TValue -- | True if the evaluated value is Bit isTBit :: TValue -> Bool -- | Produce a sequence type value tvSeq :: Nat' -> TValue -> TValue -- | Generic value type, parameterized by bit and word types. -- -- NOTE: we maintain an important invariant regarding sequence types. -- VSeq must never be used for finite sequences of bits. Always -- use the VWord constructor instead! Infinite sequences of bits -- are handled by the VStream constructor, just as for other -- types. data GenValue b w i -- | 
--   { .. }
--
VRecord :: ![(Ident, Eval (GenValue b w i))] -> GenValue b w i -- | 
--   ( .. )
--
VTuple :: ![Eval (GenValue b w i)] -> GenValue b w i -- | 
--   Bit
--
VBit :: !b -> GenValue b w i -- | Integer or Z n VInteger :: !i -> GenValue b w i -- | [n]a Invariant: VSeq is never a sequence of bits VSeq :: !Integer -> !(SeqMap b w i) -> GenValue b w i -- | 
--   [n]Bit
--
VWord :: !Integer -> !(Eval (WordValue b w i)) -> GenValue b w i -- | 
--   [inf]a
--
VStream :: !(SeqMap b w i) -> GenValue b w i -- | functions VFun :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i -- | polymorphic values (kind *) VPoly :: (TValue -> Eval (GenValue b w i)) -> GenValue b w i -- | polymorphic values (kind #) VNumPoly :: (Nat' -> Eval (GenValue b w i)) -> GenValue b w i lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i -- | A type lambda that expects a Type. tlam :: (TValue -> GenValue b w i) -> GenValue b w i -- | Generate a stream. toStream :: [GenValue b w i] -> Eval (GenValue b w i) toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i -- | Construct either a finite sequence, or a stream. In the finite case, -- record whether or not the elements were bits, to aid pretty-printing. toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i) -- | Extract a bit value. fromVBit :: GenValue b w i -> b -- | Extract a function from a value. fromVFun :: GenValue b w i -> (Eval (GenValue b w i) -> Eval (GenValue b w i)) -- | Extract a polymorphic function from a value. fromVPoly :: GenValue b w i -> (TValue -> Eval (GenValue b w i)) -- | Extract a tuple from a value. fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)] -- | Extract a record from a value. fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))] -- | Lookup a field in a record. lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i) -- | Extract a sequence. fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i) -- | Extract a packed word. fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w evalPanic :: String -> [String] -> a iteSValue :: SBool -> Value -> Value -> Eval Value mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool) mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) instance Cryptol.Eval.Value.BitWord Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord Cryptol.Symbolic.Value.SInteger module Cryptol.Eval.Env data GenEvalEnv b w i EvalEnv :: !(Map Name (Eval (GenValue b w i))) -> !TypeEnv -> GenEvalEnv b w i [envVars] :: GenEvalEnv b w i -> !(Map Name (Eval (GenValue b w i))) [envTypes] :: GenEvalEnv b w i -> !TypeEnv ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc -- | Evaluation environment with no bindings emptyEnv :: GenEvalEnv b w i -- | Bind a variable in the evaluation environment. bindVar :: Name -> Eval (GenValue b w i) -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i) -- | Bind a variable to a value in the evaluation environment, without -- creating a thunk. bindVarDirect :: Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i -- | Lookup a variable in the environment. lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i)) -- | Bind a type variable of kind *. bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i -- | Lookup a type variable. lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue) instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData i, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Env.GenEvalEnv b w i) instance GHC.Generics.Generic (Cryptol.Eval.Env.GenEvalEnv b w i) instance GHC.Base.Semigroup (Cryptol.Eval.Env.GenEvalEnv b w i) instance GHC.Base.Monoid (Cryptol.Eval.Env.GenEvalEnv b w i) module Cryptol.Eval -- | Extend the given evaluation environment with all the declarations -- contained in the given module. moduleEnv :: EvalPrims b w i => Module -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i) -- | Execute the given evaluation action. runEval :: EvalOpts -> Eval a -> IO a -- | Some options for evalutaion data EvalOpts EvalOpts :: Logger -> PPOpts -> EvalOpts -- | Where to print stuff (e.g., for trace) [evalLogger] :: EvalOpts -> Logger -- | How to pretty print things. [evalPPOpts] :: EvalOpts -> PPOpts -- | How to pretty print things when evaluating data PPOpts PPOpts :: Bool -> Int -> Int -> PPOpts [useAscii] :: PPOpts -> Bool [useBase] :: PPOpts -> Int [useInfLength] :: PPOpts -> Int defaultPPOpts :: PPOpts -- | The monad for Cryptol evaluation. data Eval a type EvalEnv = GenEvalEnv Bool BV Integer -- | Evaluation environment with no bindings emptyEnv :: GenEvalEnv b w i -- | Evaluate a Cryptol expression to a value. This evaluator is -- parameterized by the EvalPrims class, which defines the -- behavior of bits and words, in addition to providing implementations -- for all the primitives. evalExpr :: EvalPrims b w i => GenEvalEnv b w i -> Expr -> Eval (GenValue b w i) -- | Extend the given evaluation environment with the result of evaluating -- the given collection of declaration groups. evalDecls :: EvalPrims b w i => [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i) -- | Data type describing errors that can occur during evaluation. data EvalError -- | Out-of-bounds index InvalidIndex :: Integer -> EvalError -- | Non-numeric type passed to number function TypeCannotBeDemoted :: Type -> EvalError -- | Division or modulus by 0 DivideByZero :: EvalError -- | Exponentiation by negative integer NegativeExponent :: EvalError -- | Logarithm of a negative integer LogNegative :: EvalError -- | Bitvector too large WordTooWide :: Integer -> EvalError -- | Call to the Cryptol error primitive UserError :: String -> EvalError -- | Detectable nontermination LoopError :: String -> EvalError -- | Force the evaluation of a value forceValue :: GenValue b w i -> Eval () instance GHC.Base.Semigroup (Cryptol.Eval.ListEnv b w i) instance GHC.Base.Monoid (Cryptol.Eval.ListEnv b w i) module Cryptol.Utils.Patterns newtype Match b Match :: (forall r. r -> (b -> r) -> r) -> Match b type Pat a b = a -> Match b (|||) :: Pat a b -> Pat a b -> Pat a b -- | Check that a value satisfies multiple patterns. For example, an "as" -- pattern is (__ &&& p). (&&&) :: Pat a b -> Pat a c -> Pat a (b, c) -- | Match a value, and modify the result. (~>) :: Pat a b -> (b -> c) -> Pat a c -- | Match a value, and return the given result (~~>) :: Pat a b -> c -> Pat a c -- | View pattern. (<~) :: (a -> b) -> Pat b c -> Pat a c -- | Variable pattern. __ :: Pat a a -- | Constant pattern. succeed :: a -> Pat x a -- | Predicate pattern checkThat :: (a -> Bool) -> Pat a () -- | Check for exact value. lit :: Eq a => a -> Pat a () -- | Match a pattern, using the given default if valure. matchDefault :: a -> Match a -> a -- | Match an irrefutable pattern. Crashes on faliure. match :: Match a -> a matchMaybe :: Match a -> Maybe a list :: [Pat a b] -> Pat [a] [b] (><) :: Pat a b -> Pat x y -> Pat (a, x) (b, y) class Matches thing pats res | pats -> thing res matches :: Matches thing pats res => thing -> pats -> Match res instance (f ~ Cryptol.Utils.Patterns.Pat a a1', a1 ~ Cryptol.Utils.Patterns.Pat a1' r1) => Cryptol.Utils.Patterns.Matches a (f, a1) r1 instance (op ~ Cryptol.Utils.Patterns.Pat a (a1', a2'), a1 ~ Cryptol.Utils.Patterns.Pat a1' r1, a2 ~ Cryptol.Utils.Patterns.Pat a2' r2) => Cryptol.Utils.Patterns.Matches a (op, a1, a2) (r1, r2) instance (op ~ Cryptol.Utils.Patterns.Pat a (a1', a2', a3'), a1 ~ Cryptol.Utils.Patterns.Pat a1' r1, a2 ~ Cryptol.Utils.Patterns.Pat a2' r2, a3 ~ Cryptol.Utils.Patterns.Pat a3' r3) => Cryptol.Utils.Patterns.Matches a (op, a1, a2, a3) (r1, r2, r3) instance GHC.Base.Functor Cryptol.Utils.Patterns.Match instance GHC.Base.Applicative Cryptol.Utils.Patterns.Match instance GHC.Base.Monad Cryptol.Utils.Patterns.Match instance GHC.Base.Alternative Cryptol.Utils.Patterns.Match instance GHC.Base.MonadPlus Cryptol.Utils.Patterns.Match module Cryptol.TypeCheck.TypePat aInf :: Pat Type () aNat :: Pat Type Integer aNat' :: Pat Type Nat' anAdd :: Pat Type (Type, Type) (|-|) :: Pat Type (Type, Type) aMul :: Pat Type (Type, Type) (|^|) :: Pat Type (Type, Type) (|/|) :: Pat Type (Type, Type) (|%|) :: Pat Type (Type, Type) aMin :: Pat Type (Type, Type) aMax :: Pat Type (Type, Type) aWidth :: Pat Type Type aCeilDiv :: Pat Type (Type, Type) aCeilMod :: Pat Type (Type, Type) aLenFromThen :: Pat Type (Type, Type, Type) aLenFromThenTo :: Pat Type (Type, Type, Type) aLiteral :: Pat Prop (Type, Type) aLogic :: Pat Prop Type aTVar :: Pat Type TVar aFreeTVar :: Pat Type TVar aBit :: Pat Type () aSeq :: Pat Type (Type, Type) aWord :: Pat Type Type aChar :: Pat Type () aTuple :: Pat Type [Type] aRec :: Pat Type [(Ident, Type)] (|->|) :: Pat Type (Type, Type) aFin :: Pat Prop Type (|=|) :: Pat Prop (Type, Type) (|/=|) :: Pat Prop (Type, Type) (|>=|) :: Pat Prop (Type, Type) aCmp :: Pat Prop Type aArith :: Pat Prop Type aAnd :: Pat Prop (Prop, Prop) aTrue :: Pat Prop () anError :: Kind -> Pat Type TCErrorMessage module Cryptol.TypeCheck.SimpType tRebuild' :: Bool -> Type -> Type tRebuild :: Type -> Type tAdd :: Type -> Type -> Type tSub :: Type -> Type -> Type tMul :: Type -> Type -> Type tDiv :: Type -> Type -> Type tMod :: Type -> Type -> Type tCeilDiv :: Type -> Type -> Type tCeilMod :: Type -> Type -> Type tExp :: Type -> Type -> Type tMin :: Type -> Type -> Type tMax :: Type -> Type -> Type tWidth :: Type -> Type tLenFromThen :: Type -> Type -> Type -> Type tLenFromThenTo :: Type -> Type -> Type -> Type total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat') op1 :: (a -> b) -> [a] -> b op2 :: (a -> a -> b) -> [a] -> b op3 :: (a -> a -> a -> b) -> [a] -> b -- | Common checks: check for error, or simple full evaluation. tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type module Cryptol.TypeCheck.Solver.Utils -- | All ways to split a type in the form: `a + t1`, where a is a -- variable. splitVarSummands :: Type -> [(TVar, Type)] -- | Check if we can express a type in the form: `a + t1`. splitVarSummand :: TVar -> Type -> Maybe Type -- | Check if we can express a type in the form: `k + t1`, where k -- is a constant > 0. This assumes that the type has been simplified -- already, so that constants are floated to the left. splitConstSummand :: Type -> Maybe (Integer, Type) -- | Check if we can express a type in the form: `k * t1`, where k -- is a constant > 1 This assumes that the type has been simplified -- already, so that constants are floated to the left. splitConstFactor :: Type -> Maybe (Integer, Type) -- | Solving class constraints. module Cryptol.TypeCheck.Solver.Class -- | Solve class constraints. If not, then we return Nothing. If -- solved, then we return Just a list of sub-goals. classStep :: Prop -> Solved -- | Solve a Zero constraint by instance, if possible. solveZeroInst :: Type -> Solved -- | Solve a Logic constraint by instance, if possible. solveLogicInst :: Type -> Solved -- | Solve an Arith constraint by instance, if possible. solveArithInst :: Type -> Solved -- | Solve Cmp constraints. solveCmpInst :: Type -> Solved -- | Solve SignedCmp constraints. solveSignedCmpInst :: Type -> Solved -- | Solve Literal constraints. solveLiteralInst :: Type -> Type -> Solved -- | Add propositions that are implied by the given one. The result -- contains the orignal proposition, and maybe some more. expandProp :: Prop -> [Prop] -- | This module generates random values for Cryptol types. module Cryptol.Testing.Random type Gen g b w i = Integer -> g -> (GenValue b w i, g) -- | Apply a testable value to some randomly-generated arguments. Returns -- Nothing if the function returned True, or `Just -- counterexample` if it returned False. -- -- Please note that this function assumes that the generators match the -- supplied value, otherwise we'll panic. runOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Bool BV Integer] -> Integer -> g -> IO (TestResult, g) -- | Given a (function) type, compute generators for the function's -- arguments. Currently we do not support polymorphic functions. In -- principle, we could apply these to random types, and test the results. testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV Integer] -- | A generator for values of the given type. This fails if we are given a -- type that lacks a suitable random value generator. randomValue :: (BitWord b w i, RandomGen g) => Type -> Maybe (Gen g b w i) -- | Generate a random bit value. randomBit :: (BitWord b w i, RandomGen g) => Gen g b w i randomSize :: RandomGen g => Int -> Int -> g -> (Int, g) -- | Generate a random integer value. The size parameter is assumed to vary -- between 1 and 100, and we use it to generate smaller numbers first. randomInteger :: (BitWord b w i, RandomGen g) => Gen g b w i randomIntMod :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i -- | Generate a random word of the given length (i.e., a value of type -- [w]) The size parameter is assumed to vary between 1 and 100, -- and we use it to generate smaller numbers first. randomWord :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i -- | Generate a random infinite stream value. randomStream :: RandomGen g => Gen g b w i -> Gen g b w i -- | Generate a random sequence. This should be used for sequences other -- than bits. For sequences of bits use "randomWord". randomSequence :: RandomGen g => Integer -> Gen g b w i -> Gen g b w i -- | Generate a random tuple value. randomTuple :: RandomGen g => [Gen g b w i] -> Gen g b w i -- | Generate a random record value. randomRecord :: RandomGen g => [(Ident, Gen g b w i)] -> Gen g b w i module Cryptol.Prims.Eval primTable :: Map Ident Value -- | Make a numeric literal value at the given type. mkLit :: BitWord b w i => TValue -> Integer -> GenValue b w i -- | Make a numeric constant. ecNumberV :: BitWord b w i => GenValue b w i -- | Convert a word to a non-negative integer. ecToIntegerV :: BitWord b w i => GenValue b w i -- | Convert an unbounded integer to a packed bitvector. ecFromIntegerV :: BitWord b w i => (Integer -> i -> i) -> GenValue b w i -- | Create a packed word modExp :: Integer -> BV -> BV -> Eval BV intModExp :: Integer -> Integer -> Integer -> Eval Integer integerExp :: Integer -> Integer -> Eval Integer integerLg2 :: Integer -> Eval Integer integerNeg :: Integer -> Eval Integer intModNeg :: Integer -> Integer -> Eval Integer doubleAndAdd :: Integer -> Integer -> Integer -> Integer type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i) binary :: Binary b w i -> GenValue b w i type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i) unary :: Unary b w i -> GenValue b w i -- | Turn a normal binop on Integers into one that can also deal with a -- bitsize. However, if the bitvector size is 0, always return the 0 -- bitvector. liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV -- | Turn a normal binop on Integers into one that can also deal with a -- bitsize. Generate a thunk that throws a divide by 0 error when forced -- if the second argument is 0. However, if the bitvector size is 0, -- always return the 0 bitvector. liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV type BinArith w = Integer -> w -> w -> Eval w liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer liftBinIntMod :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> Eval Integer liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer modWrap :: Integral a => a -> a -> Eval a arithBinary :: forall b w i. BitWord b w i => BinArith w -> (i -> i -> Eval i) -> (Integer -> i -> i -> Eval i) -> Binary b w i type UnaryArith w = Integer -> w -> Eval w liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV arithUnary :: forall b w i. BitWord b w i => UnaryArith w -> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i arithNullary :: forall b w i. BitWord b w i => (Integer -> w) -> i -> (Integer -> i) -> TValue -> GenValue b w i lg2 :: Integer -> Integer addV :: BitWord b w i => Binary b w i subV :: BitWord b w i => Binary b w i mulV :: BitWord b w i => Binary b w i intV :: BitWord b w i => i -> TValue -> GenValue b w i cmpValue :: BitWord b w i => (b -> b -> Eval a -> Eval a) -> (w -> w -> Eval a -> Eval a) -> (i -> i -> Eval a -> Eval a) -> (Integer -> i -> i -> Eval a -> Eval a) -> (TValue -> GenValue b w i -> GenValue b w i -> Eval a -> Eval a) lexCompare :: TValue -> Value -> Value -> Eval Ordering signedLexCompare :: TValue -> Value -> Value -> Eval Ordering -- | Process two elements based on their lexicographic ordering. cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer -- | Process two elements based on their lexicographic ordering, using -- signed comparisons signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer -- | Lifted operation on finite bitsequences. Used for signed comparisons -- and arithemtic. liftWord :: BitWord b w i => (w -> w -> Eval (GenValue b w i)) -> GenValue b w i liftSigned :: (Integer -> Integer -> Integer -> Eval BV) -> BinArith BV signedBV :: BV -> Integer signedValue :: Integer -> Integer -> Integer bvSlt :: Integer -> Integer -> Integer -> Eval Value bvSdiv :: Integer -> Integer -> Integer -> Eval BV bvSrem :: Integer -> Integer -> Integer -> Eval BV sshrV :: Value -- | Signed carry bit. scarryV :: Value -- | Unsigned carry bit. carryV :: Value zeroV :: forall b w i. BitWord b w i => TValue -> GenValue b w i joinWordVal :: BitWord b w i => WordValue b w i -> WordValue b w i -> WordValue b w i joinWords :: forall b w i. BitWord b w i => Integer -> Integer -> SeqMap b w i -> Eval (GenValue b w i) joinSeq :: BitWord b w i => Nat' -> Integer -> TValue -> SeqMap b w i -> Eval (GenValue b w i) -- | Join a sequence of sequences into a single sequence. joinV :: BitWord b w i => Nat' -> Integer -> TValue -> GenValue b w i -> Eval (GenValue b w i) splitWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> (WordValue b w i, WordValue b w i) splitAtV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i) extractWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> WordValue b w i -- | Split implementation. ecSplitV :: BitWord b w i => GenValue b w i reverseV :: forall b w i. BitWord b w i => GenValue b w i -> Eval (GenValue b w i) transposeV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i) ccatV :: (Show b, Show w, BitWord b w i) => Nat' -> Nat' -> TValue -> (GenValue b w i) -> (GenValue b w i) -> Eval (GenValue b w i) wordValLogicOp :: BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> WordValue b w i -> WordValue b w i -> Eval (WordValue b w i) -- | Merge two values given a binop. This is used for and, or and xor. logicBinary :: forall b w i. BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> Binary b w i wordValUnaryOp :: BitWord b w i => (b -> b) -> (w -> w) -> WordValue b w i -> Eval (WordValue b w i) logicUnary :: forall b w i. BitWord b w i => (b -> b) -> (w -> w) -> Unary b w i logicShift :: (Integer -> Integer -> Integer -> Integer) -> (Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)) -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) -> Value shiftLW :: Integer -> Integer -> Integer -> Integer shiftLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap shiftRW :: Integer -> Integer -> Integer -> Integer shiftRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap rotateLW :: Integer -> Integer -> Integer -> Integer rotateLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap rotateRW :: Integer -> Integer -> Integer -> Integer rotateRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap -- | Indexing operations. indexPrim :: BitWord b w i => (Maybe Integer -> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i)) -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i)) -> GenValue b w i indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value updateFront :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer) updateFront_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer) updateBack :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer) updateBack_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer) updatePrim :: BitWord b w i => (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i)) -> (Nat' -> TValue -> SeqMap b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i)) -> GenValue b w i fromThenV :: BitWord b w i => GenValue b w i fromToV :: BitWord b w i => GenValue b w i fromThenToV :: BitWord b w i => GenValue b w i infFromV :: BitWord b w i => GenValue b w i infFromThenV :: BitWord b w i => GenValue b w i -- | Produce a random value with the given seed. If we do not support -- making values of the given type, return zero of that type. TODO: do -- better than returning zero randomV :: BitWord b w i => TValue -> Integer -> GenValue b w i errorV :: forall b w i. BitWord b w i => TValue -> String -> Eval (GenValue b w i) instance Cryptol.Eval.Value.EvalPrims GHC.Types.Bool Cryptol.Eval.Value.BV GHC.Integer.Type.Integer module Cryptol.Symbolic.Prims traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) primTable :: Map Ident Value -- | Barrel-shifter algorithm. Takes a list of bits in big-endian order. shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value selectV :: forall a. (SBool -> Eval a -> Eval a -> Eval a) -> WordValue SBool SWord SInteger -> (Integer -> Eval a) -> Eval a indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger) updateFrontSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger) updateBackSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) asBitList :: [Eval SBool] -> Maybe [SBool] asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord] liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord liftBin :: (a -> b -> c) -> a -> b -> Eval c liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a sExp :: Integer -> SWord -> SWord -> Eval SWord sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger -- | Ceiling (log_2 x) sLg2 :: Integer -> SWord -> Eval SWord -- | Ceiling (log_2 x) svLg2 :: SInteger -> Eval SInteger svModLg2 :: Integer -> SInteger -> Eval SInteger cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool cmpLt :: SWord -> SWord -> Eval SBool -> Eval SBool cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool cmpLtEq :: SWord -> SWord -> Eval SBool -> Eval SBool cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool cmpMod :: (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool) cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool svDivisible :: Integer -> SInteger -> SBool cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) -> (SWord -> SWord -> Eval SBool -> Eval SBool) -> (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool) -> SBool -> Binary SBool SWord SInteger signedQuot :: SWord -> SWord -> SWord signedRem :: SWord -> SWord -> SWord sshrV :: Value carry :: SWord -> SWord -> Eval Value scarry :: SWord -> SWord -> Eval Value instance Cryptol.Eval.Value.EvalPrims Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord Cryptol.Symbolic.Value.SInteger module Cryptol.TypeCheck.Solver.Numeric -- | Try to solve t1 = t2 cryIsEqual :: Ctxt -> Type -> Type -> Solved -- | Try to solve t1 /= t2 cryIsNotEqual :: Ctxt -> Type -> Type -> Solved -- | Try to solve t1 >= t2 cryIsGeq :: Ctxt -> Type -> Type -> Solved module Cryptol.TypeCheck.SimpleSolver simplify :: Ctxt -> Prop -> Prop simplifyStep :: Ctxt -> Prop -> Solved module Cryptol.TypeCheck.Subst -- | Type Subst has an invariant on its suMap component: 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. data Subst emptySubst :: Subst singleSubst :: TVar -> Type -> Subst (@@) :: Subst -> Subst -> Subst defaultingSubst :: Subst -> Subst -- | 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 isEmptySubst :: Subst -> Bool class FVS t fvs :: FVS t => t -> Set TVar -- | Apply a substitution. Returns Nothing if nothing changed. apSubstMaybe :: Subst -> Type -> Maybe Type class TVars t apSubst :: TVars t => Subst -> t -> t -- | Apply the substitution to the keys of a type map. apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a substBinds :: Subst -> Set TVar applySubstToVar :: Subst -> TVar -> Maybe Type substToList :: Subst -> [(TVar, Type)] instance GHC.Show.Show Cryptol.TypeCheck.Subst.Subst instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars (GHC.Base.Maybe t) instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars [t] instance (Cryptol.TypeCheck.Subst.TVars s, Cryptol.TypeCheck.Subst.TVars t) => Cryptol.TypeCheck.Subst.TVars (s, t) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Type.Type instance (GHC.Base.Functor m, Cryptol.TypeCheck.Subst.TVars a) => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.List m a) instance Cryptol.TypeCheck.Subst.TVars a => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.TypeMap a) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Type.Schema instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Expr instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Match instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Decl instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclDef instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Subst.Subst) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Subst.Subst module Cryptol.TypeCheck.Unify -- | The most general unifier is a substitution and a set of constraints on -- bound variables. type MGU = (Subst, [Prop]) type Result a = Writer [UnificationError] a runResult :: Result a -> (a, [UnificationError]) data UnificationError UniTypeMismatch :: Type -> Type -> UnificationError UniKindMismatch :: Kind -> Kind -> UnificationError UniTypeLenMismatch :: Int -> Int -> UnificationError UniRecursive :: TVar -> Type -> UnificationError UniNonPolyDepends :: TVar -> [TParam] -> UnificationError UniNonPoly :: TVar -> Type -> UnificationError uniError :: UnificationError -> Result MGU emptyMGU :: MGU mgu :: Type -> Type -> Result MGU mguMany :: [Type] -> [Type] -> Result MGU bindVar :: TVar -> Type -> Result MGU freeParams :: FVS t => t -> Set TParam module Cryptol.TypeCheck.TypeOf -- | Given a typing environment and an expression, compute the type of the -- expression as quickly as possible, assuming that the expression is -- well formed with correct type annotations. fastTypeOf :: Map Name Schema -> Expr -> Type fastSchemaOf :: Map Name Schema -> Expr -> Schema -- | Assumes that local names do not shadow top level names. module Cryptol.ModuleSystem.InstantiateModule -- | Convert a module instantiation into a partial module. The resulting -- module is incomplete because it is missing the definitions from the -- instantiation. instantiateModule :: FreshM m => Module -> ModName -> Map TParam Type -> Map Name Expr -> m ([Located Prop], Module) instance GHC.Show.Show Cryptol.ModuleSystem.InstantiateModule.Env instance Cryptol.ModuleSystem.InstantiateModule.Inst a => Cryptol.ModuleSystem.InstantiateModule.Inst [a] instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Expr instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.DeclDef instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Decl instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Match instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Schema instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Type instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.Prims.Syntax.TCon instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.Prims.Syntax.TC instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.Prims.Syntax.UserTC instance Cryptol.ModuleSystem.InstantiateModule.Inst (Cryptol.ModuleSystem.Exports.ExportSpec Cryptol.ModuleSystem.Name.Name) instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.TySyn instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Newtype instance Cryptol.ModuleSystem.InstantiateModule.Defines t => Cryptol.ModuleSystem.InstantiateModule.Defines [t] instance Cryptol.ModuleSystem.InstantiateModule.Defines Cryptol.TypeCheck.AST.Decl instance Cryptol.ModuleSystem.InstantiateModule.Defines Cryptol.TypeCheck.AST.DeclGroup -- | Look for opportunity to solve goals by instantiating variables. module Cryptol.TypeCheck.Solver.Improve -- | Improvements from a bunch of propositions. Invariant: the substitions -- should be already applied to the new sub-goals, if any. improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst, [Prop]) -- | Improvements from a proposition. Invariant: the substitions should be -- already applied to the new sub-goals, if any. improveProp :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop]) improveLit :: Bool -> Prop -> Match (Subst, [Prop]) -- | Improvements from equality constraints. Invariant: the substitions -- should be already applied to the new sub-goals, if any. improveEq :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop]) -- | This module contains types used during type inference. module Cryptol.TypeCheck.InferTypes data SolverConfig SolverConfig :: FilePath -> [String] -> Int -> [FilePath] -> SolverConfig -- | The SMT solver to invoke [solverPath] :: SolverConfig -> FilePath -- | Additional arguments to pass to the solver [solverArgs] :: SolverConfig -> [String] -- | How verbose to be when type-checking [solverVerbose] :: SolverConfig -> Int -- | Look for the solver prelude in these locations. [solverPreludePath] :: SolverConfig -> [FilePath] -- | The types of variables in the environment. data VarType -- | Known type ExtVar :: Schema -> VarType -- | Part of current SCC. The expression will replace the variable, after -- we are done with the SCC. In this way a variable that gets generalized -- is replaced with an appropriate instantiation of itself. CurSCC :: Expr -> Type -> VarType data Goals Goals :: Set Goal -> Map TVar LitGoal -> Goals -- | A bunch of goals, not including the ones in literalGoals. [goalSet] :: Goals -> Set Goal -- | An entry (a,t) corresponds to Literal t a. [literalGoals] :: Goals -> Map TVar LitGoal -- | This abuses the type Goal a bit. The goal field contains -- only the numeric part of the Literal constraint. For example, (a, -- Goal { goal = t }) representats the goal for Literal t a type LitGoal = Goal litGoalToGoal :: (TVar, LitGoal) -> Goal goalToLitGoal :: Goal -> Maybe (TVar, LitGoal) emptyGoals :: Goals nullGoals :: Goals -> Bool fromGoals :: Goals -> [Goal] goalsFromList :: [Goal] -> Goals insertGoal :: Goal -> Goals -> Goals -- | Something that we need to find evidence for. data Goal Goal :: ConstraintSource -> Range -> Prop -> Goal -- | What it is about [goalSource] :: Goal -> ConstraintSource -- | Part of source code that caused goal [goalRange] :: Goal -> Range -- | What needs to be proved [goal] :: Goal -> Prop data HasGoal HasGoal :: !Int -> Goal -> HasGoal [hasName] :: HasGoal -> !Int [hasGoal] :: HasGoal -> Goal -- | Delayed implication constraints, arising from user-specified type -- sigs. data DelayedCt DelayedCt :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt -- | Signature that gave rise to this constraint Nothing means module -- top-level [dctSource] :: DelayedCt -> Maybe Name [dctForall] :: DelayedCt -> [TParam] [dctAsmps] :: DelayedCt -> [Prop] [dctGoals] :: DelayedCt -> [Goal] -- | Information about how a constraint came to be, used in error -- reporting. data ConstraintSource -- | Computing shape of list comprehension CtComprehension :: ConstraintSource -- | Use of a split pattern CtSplitPat :: ConstraintSource -- | A type signature in a pattern or expression CtTypeSig :: ConstraintSource -- | Instantiation of this expression CtInst :: Expr -> ConstraintSource CtSelector :: ConstraintSource CtExactType :: ConstraintSource CtEnumeration :: ConstraintSource -- | Just defaulting on the command line CtDefaulting :: ConstraintSource -- | Use of a partial type function. CtPartialTypeFun :: TyFunName -> ConstraintSource CtImprovement :: ConstraintSource -- | Constraints arising from type-checking patterns CtPattern :: Doc -> ConstraintSource -- | Instantiating a parametrized module CtModuleInstance :: ModName -> ConstraintSource data TyFunName UserTyFun :: Name -> TyFunName BuiltInTyFun :: TFun -> TyFunName BuiltInTC :: TC -> TyFunName -- | For use in error messages cppKind :: Kind -> Doc addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc ppUse :: Expr -> Doc instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goals instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.HasGoal instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.DelayedCt instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.DelayedCt instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.DelayedCt instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.Goal instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.Goal instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goal instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.ConstraintSource instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.ConstraintSource instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.ConstraintSource instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.TyFunName instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.TyFunName instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.TyFunName instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.SolverConfig instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.SolverConfig instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.SolverConfig instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goals instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.HasGoal instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.DelayedCt instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.DelayedCt instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.DelayedCt) instance GHC.Classes.Eq Cryptol.TypeCheck.InferTypes.Goal instance GHC.Classes.Ord Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Goal) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.ConstraintSource instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.ConstraintSource instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.TyFunName module Cryptol.TypeCheck.Solver.SMT -- | An SMT solver packed with a logger for debugging. data Solver -- | Execute a computation with a fresh solver instance. withSolver :: SolverConfig -> (Solver -> IO a) -> IO a -- | Assumes no And isNumeric :: Prop -> Bool debugBlock :: Solver -> String -> IO a -> IO a debugLog :: DebugLog t => Solver -> t -> IO () -- | Returns goals that were not proved proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal] -- | Check if the given goals are known to be unsolvable. checkUnsolvable :: Solver -> [Goal] -> IO Bool tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')]) shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')] instance Cryptol.TypeCheck.Solver.SMT.Mk () instance Cryptol.TypeCheck.Solver.SMT.Mk GHC.Integer.Type.Integer instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.TVar instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.Type instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.Prims.Syntax.TCErrorMessage instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type) instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type) instance Cryptol.TypeCheck.Solver.SMT.DebugLog GHC.Types.Char instance Cryptol.TypeCheck.Solver.SMT.DebugLog a => Cryptol.TypeCheck.Solver.SMT.DebugLog [a] instance Cryptol.TypeCheck.Solver.SMT.DebugLog a => Cryptol.TypeCheck.Solver.SMT.DebugLog (GHC.Base.Maybe a) instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.Utils.PP.Doc instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.Type.Type instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.Subst.Subst module Cryptol.TypeCheck.Error cleanupErrors :: [(Range, Error)] -> [(Range, Error)] -- | Should the first error suppress the next one. subsumes :: Error -> Error -> Bool data Warning DefaultingKind :: (TParam Name) -> Kind -> Warning DefaultingWildType :: Kind -> Warning DefaultingTo :: TVarInfo -> Type -> Warning -- | Various errors that might happen during type checking/inference data Error -- | Just say this ErrorMsg :: Doc -> Error -- | Expected kind, inferred kind KindMismatch :: Kind -> Kind -> Error -- | Number of extra parameters, kind of result (which should not be of the -- form _ -> _) TooManyTypeParams :: Int -> Kind -> Error -- | A type variable was applied to some arguments. TyVarWithParams :: Error -- | Type-synonym, number of extra params TooManyTySynParams :: Name -> Int -> Error -- | Type-synonym, number of missing params TooFewTySynParams :: Name -> Int -> Error -- | The type synonym declarations are recursive RecursiveTypeDecls :: [Name] -> Error -- | Expected type, inferred type TypeMismatch :: Type -> Type -> Error -- | Unification results in a recursive type RecursiveType :: Type -> Type -> Error -- | A constraint that we could not solve The boolean indicates if we know -- that this constraint is impossible. UnsolvedGoals :: Bool -> [Goal] -> Error -- | A constraint (with context) that we could not solve UnsolvedDelayedCt :: DelayedCt -> Error -- | Type wild cards are not allowed in this context (e.g., definitions of -- type synonyms). UnexpectedTypeWildCard :: Error -- | Unification variable depends on quantified variables that are not in -- scope. TypeVariableEscaped :: Type -> [TParam] -> Error -- | Quantified type variables (of kind *) need to match the given type, so -- it does not work for all types. NotForAll :: TVar -> Type -> Error -- | The given constraints causes the signature of the function to be -- not-satisfiable. UnusableFunction :: Name -> [Prop] -> Error -- | Too many positional type arguments, in an explicit type instantiation TooManyPositionalTypeParams :: Error CannotMixPositionalAndNamedTypeParams :: Error UndefinedTypeParameter :: (Located Ident) -> Error RepeatedTypeParameter :: Ident -> [Range] -> Error AmbiguousType :: [Name] -> [TVar] -> Error instance Control.DeepSeq.NFData Cryptol.TypeCheck.Error.Error instance GHC.Generics.Generic Cryptol.TypeCheck.Error.Error instance GHC.Show.Show Cryptol.TypeCheck.Error.Error instance Control.DeepSeq.NFData Cryptol.TypeCheck.Error.Warning instance GHC.Generics.Generic Cryptol.TypeCheck.Error.Warning instance GHC.Show.Show Cryptol.TypeCheck.Error.Warning instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Error.Error instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Error.Error instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Error.Error instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Error.Error) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Error.Warning instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Error.Warning instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Error.Warning instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Error.Warning) module Cryptol.TypeCheck.Monad -- | This is what's returned when we lookup variables during kind checking. data LkpTyVar -- | Locally bound variable. TLocalVar :: TParam -> (Maybe Kind) -> LkpTyVar -- | An outer binding. TOuterVar :: TParam -> LkpTyVar data KRW KRW :: Map Name Kind -> [(ConstraintSource, [Prop])] -> KRW -- | kinds of (known) vars. [typeParams] :: KRW -> Map Name Kind [kCtrs] :: KRW -> [(ConstraintSource, [Prop])] -- | Do we allow wild cards in the given context. data AllowWildCards AllowWildCards :: AllowWildCards NoWildCards :: AllowWildCards data KRO KRO :: Map Name TParam -> AllowWildCards -> KRO -- | lazy map, with tparams. [lazyTParams] :: KRO -> Map Name TParam -- | are type-wild cards allowed? [allowWild] :: KRO -> AllowWildCards newtype KindM a KM :: ReaderT KRO (StateT KRW InferM) a -> KindM a [unKM] :: KindM a -> ReaderT KRO (StateT KRW InferM) a -- | Read-write component of the monad. data RW RW :: ![(Range, Error)] -> ![(Range, Warning)] -> !Subst -> [Map Name Type] -> Map Int (Expr -> Expr) -> !NameSeeds -> !Goals -> ![HasGoal] -> !Supply -> RW -- | Collected errors [iErrors] :: RW -> ![(Range, Error)] -- | Collected warnings [iWarnings] :: RW -> ![(Range, Warning)] -- | Accumulated substitution [iSubst] :: RW -> !Subst -- | These keeps track of what existential type variables are available. -- When we start checking a function, we push a new scope for its -- arguments, and we pop it when we are done checking the function body. -- The front element of the list is the current scope, which is the only -- thing that will be modified, as follows. When we encounter a -- existential type variable: 1. we look in all scopes to see if it is -- already defined. 2. if it was not defined, we create a fresh type -- variable, and we add it to the current scope. 3. it is an error if we -- encounter an existential variable but we have no current scope. [iExistTVars] :: RW -> [Map Name Type] -- | Selector constraints that have been solved (ref. iSolvedSelectorsLazy) [iSolvedHas] :: RW -> Map Int (Expr -> Expr) [iNameSeeds] :: RW -> !NameSeeds -- | Ordinary constraints [iCts] :: RW -> !Goals -- | Tuple/record projection constraints. The Int is the "name" of -- the constraint, used so that we can name it solution properly. [iHasCts] :: RW -> ![HasGoal] [iSupply] :: RW -> !Supply -- | Read-only component of the monad. data RO RO :: Range -> Map Name VarType -> [TParam] -> Map Name (DefLoc, TySyn) -> Map Name (DefLoc, Newtype) -> Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> Map Int (Expr -> Expr) -> Bool -> Solver -> !PrimMap -> !(IORef Int) -> RO -- | Source code being analysed [iRange] :: RO -> Range -- | Type of variable that are in scope [iVars] :: RO -> Map Name VarType -- | Type variable that are in scope [iTVars] :: RO -> [TParam] -- | Type synonyms that are in scope [iTSyns] :: RO -> Map Name (DefLoc, TySyn) -- | Newtype declarations in scope -- -- NOTE: type synonyms take precedence over newtype. The reason is that -- we can define local type synonyms, but not local newtypes. So, either -- a type-synonym shadows a newtype, or it was declared at the top-level, -- but then there can't be a newtype with the same name (this should be -- caught by the renamer). [iNewtypes] :: RO -> Map Name (DefLoc, Newtype) -- | Parameter types [iParamTypes] :: RO -> Map Name ModTParam -- | Constraints on the type parameters [iParamConstraints] :: RO -> [Located Prop] -- | Parameter functions [iParamFuns] :: RO -> Map Name ModVParam -- | NOTE: This field is lazy in an important way! It is the final version -- of iSolvedHas in RW, and the two are tied together -- through recursion. The field is here so that we can look thing up -- before they are defined, which is OK because we don't need to know the -- results until everything is done. [iSolvedHasLazy] :: RO -> Map Int (Expr -> Expr) -- | When this flag is set to true, bindings that lack signatures in -- where-blocks will never be generalized. Bindings with type signatures, -- and all bindings at top level are unaffected. [iMonoBinds] :: RO -> Bool [iSolver] :: RO -> Solver [iPrimNames] :: RO -> !PrimMap [iSolveCounter] :: RO -> !(IORef Int) data DefLoc IsLocal :: DefLoc IsExternal :: DefLoc newtype InferM a IM :: ReaderT RO (StateT RW IO) a -> InferM a [unIM] :: InferM a -> ReaderT RO (StateT RW IO) a -- | The results of type inference. data InferOutput a -- | We found some errors InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a -- | Type inference was successful. InferOK :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a -- | This is used for generating various names. data NameSeeds NameSeeds :: !Int -> !Int -> NameSeeds [seedTVar] :: NameSeeds -> !Int [seedGoal] :: NameSeeds -> !Int -- | Information needed for type inference. data InferInput InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> !(Map Name ModTParam) -> !([Located Prop]) -> !(Map Name ModVParam) -> NameSeeds -> Bool -> SolverConfig -> [FilePath] -> !PrimMap -> !Supply -> InferInput -- | Location of program source [inpRange] :: InferInput -> Range -- | Variables that are in scope [inpVars] :: InferInput -> Map Name Schema -- | Type synonyms that are in scope [inpTSyns] :: InferInput -> Map Name TySyn -- | Newtypes in scope [inpNewtypes] :: InferInput -> Map Name Newtype -- | Type parameters [inpParamTypes] :: InferInput -> !(Map Name ModTParam) -- | Constraints on parameters [inpParamConstraints] :: InferInput -> !([Located Prop]) -- | Value parameters [inpParamFuns] :: InferInput -> !(Map Name ModVParam) -- | Private state of type-checker [inpNameSeeds] :: InferInput -> NameSeeds -- | Should local bindings without signatures be monomorphized? [inpMonoBinds] :: InferInput -> Bool -- | Options for the constraint solver [inpSolverConfig] :: InferInput -> SolverConfig -- | Where to look for Cryptol theory file. [inpSearchPath] :: InferInput -> [FilePath] -- | This is used when the type-checker needs to refer to a predefined -- identifier (e.g., number). [inpPrimNames] :: InferInput -> !PrimMap -- | The supply for fresh name generation [inpSupply] :: InferInput -> !Supply -- | The initial seeds, used when checking a fresh program. XXX: why does -- this start at 10? nameSeeds :: NameSeeds bumpCounter :: InferM () runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) io :: IO a -> InferM a -- | The monadic computation is about the given range of source code. This -- is useful for error reporting. inRange :: Range -> InferM a -> InferM a inRangeMb :: Maybe Range -> InferM a -> InferM a -- | This is the current range that we are working on. curRange :: InferM Range -- | Report an error. recordError :: Error -> InferM () recordWarning :: Warning -> InferM () getSolver :: InferM Solver -- | Retrieve the mapping between identifiers and declarations in the -- prelude. getPrimMap :: InferM PrimMap newGoal :: ConstraintSource -> Prop -> InferM Goal -- | Record some constraints that need to be solved. The string explains -- where the constraints came from. newGoals :: ConstraintSource -> [Prop] -> InferM () -- | The constraints are removed, and returned to the caller. The -- substitution IS applied to them. getGoals :: InferM [Goal] -- | Add a bunch of goals that need solving. addGoals :: [Goal] -> InferM () -- | Collect the goals emitted by the given sub-computation. Does not emit -- any new goals. collectGoals :: InferM a -> InferM (a, [Goal]) simpGoal :: Goal -> InferM [Goal] simpGoals :: [Goal] -> InferM [Goal] -- | Record a constraint that when we select from the first type, we should -- get a value of the second type. The returned function should be used -- to wrap the expression from which we are selecting (i.e., the record -- or tuple). Plese note that the resulting expression should not be -- forced before the constraint is solved. newHasGoal :: Selector -> Type -> Type -> InferM (Expr -> Expr) -- | Add a previously generate has constrained addHasGoal :: HasGoal -> InferM () -- | Get the Has constraints. Each of this should either be -- solved, or added back using addHasGoal. getHasGoals :: InferM [HasGoal] -- | Specify the solution (`Expr -> Expr`) for the given constraint -- (Int). solveHasGoal :: Int -> (Expr -> Expr) -> InferM () -- | Generate a fresh variable name to be used in a local binding. newParamName :: Ident -> InferM Name newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a -- | Generate a new name for a goal. newGoalName :: InferM Int -- | Generate a new free type variable. newTVar :: TVarSource -> Kind -> InferM TVar -- | Generate a new free type variable that depends on these additional -- type parameters. newTVar' :: TVarSource -> Set TParam -> Kind -> InferM TVar -- | Generate a new free type variable. newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam -- | Generate an unknown type. The doc is a note about what is this type -- about. newType :: TVarSource -> Kind -> InferM Type -- | Record that the two types should be syntactically equal. unify :: Type -> Type -> InferM [Prop] -- | Apply the accumulated substitution to something with free type -- variables. applySubst :: TVars t => t -> InferM t applySubstPreds :: [Prop] -> InferM [Prop] applySubstGoals :: [Goal] -> InferM [Goal] -- | Get the substitution that we have accumulated so far. getSubst :: InferM Subst -- | Add to the accumulated substitution, checking that the datatype -- invariant for Subst is maintained. extendSubst :: Subst -> InferM () -- | Variables that are either mentioned in the environment or in a -- selector constraint. varsWithAsmps :: InferM (Set TVar) -- | Lookup the type of a variable. lookupVar :: Name -> InferM VarType -- | Lookup a type variable. Return Nothing if there is no such -- variable in scope, in which case we must be dealing with a type -- constant. lookupTParam :: Name -> InferM (Maybe TParam) -- | Lookup the definition of a type synonym. lookupTSyn :: Name -> InferM (Maybe TySyn) -- | Lookup the definition of a newtype lookupNewtype :: Name -> InferM (Maybe Newtype) -- | Lookup the kind of a parameter type lookupParamType :: Name -> InferM (Maybe ModTParam) -- | Lookup the schema for a parameter function. lookupParamFun :: Name -> InferM (Maybe ModVParam) -- | Check if we already have a name for this existential type variable -- and, if so, return the definition. If not, try to create a new -- definition, if this is allowed. If not, returns nothing. existVar :: Name -> Kind -> InferM Type -- | Returns the type synonyms that are currently in scope. getTSyns :: InferM (Map Name (DefLoc, TySyn)) -- | Returns the newtype declarations that are in scope. getNewtypes :: InferM (Map Name (DefLoc, Newtype)) -- | Returns the parameter functions declarations getParamFuns :: InferM (Map Name ModVParam) -- | Returns the abstract function declarations getParamTypes :: InferM (Map Name ModTParam) -- | Constraints on the module's parameters. getParamConstraints :: InferM [Located Prop] -- | Get the set of bound type variables that are in scope. getTVars :: InferM (Set Name) -- | Return the keys of the bound variables that are in scope. getBoundInScope :: InferM (Set TParam) -- | Retrieve the value of the `mono-binds` option. getMonoBinds :: InferM Bool -- | We disallow shadowing between type synonyms and type variables because -- it is confusing. As a bonus, in the implementation we don't need to -- worry about where we lookup things (i.e., in the variable or type -- synonym environment. checkTShadowing :: String -> Name -> InferM () -- | The sub-computation is performed with the given type parameter in -- scope. withTParam :: TParam -> InferM a -> InferM a withTParams :: [TParam] -> InferM a -> InferM a -- | The sub-computation is performed with the given type-synonym in scope. withTySyn :: TySyn -> InferM a -> InferM a withNewtype :: Newtype -> InferM a -> InferM a withParamType :: ModTParam -> InferM a -> InferM a -- | The sub-computation is performed with the given variable in scope. withVarType :: Name -> VarType -> InferM a -> InferM a withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a withVar :: Name -> Schema -> InferM a -> InferM a -- | The sub-computation is performed with the given abstract function in -- scope. withParamFuns :: [ModVParam] -> InferM a -> InferM a -- | Add some assumptions for an entire module withParameterConstraints :: [Located Prop] -> InferM a -> InferM a -- | The sub-computation is performed with the given variables in scope. withMonoType :: (Name, Located Type) -> InferM a -> InferM a -- | The sub-computation is performed with the given variables in scope. withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a -- | The sub-computation is performed with the given type synonyms and -- variables in scope. withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a -- | Perform the given computation in a new scope (i.e., the subcomputation -- may use existential type variables). inNewScope :: InferM a -> InferM a -- | The arguments to this function are as follows: -- -- (type param. name, kind signature (opt.), type parameter) -- -- The type parameter is just a thunk that we should not force. The -- reason is that the parameter depends on the kind that we are in the -- process of computing. -- -- As a result we return the value of the sub-computation and the -- computed kinds of the type parameters. runKindM :: AllowWildCards -> [(Name, Maybe Kind, TParam)] -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])]) -- | Check if a name refers to a type variable. kLookupTyVar :: Name -> KindM (Maybe LkpTyVar) -- | Are type wild-cards OK in this context? kWildOK :: KindM AllowWildCards -- | Reports an error. kRecordError :: Error -> KindM () kRecordWarning :: Warning -> KindM () -- | Generate a fresh unification variable of the given kind. NOTE: We do -- not simplify these, because we end up with bottom. See hs XXX: -- Perhaps we can avoid the recursion? kNewType :: TVarSource -> Kind -> KindM Type -- | Lookup the definition of a type synonym. kLookupTSyn :: Name -> KindM (Maybe TySyn) -- | Lookup the definition of a newtype. kLookupNewtype :: Name -> KindM (Maybe Newtype) kLookupParamType :: Name -> KindM (Maybe ModTParam) kExistTVar :: Name -> Kind -> KindM Type -- | Replace the given bound variables with concrete types. kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type -- | Record the kind for a local type variable. This assumes that we -- already checked that there was no other valid kind for the variable -- (if there was one, it gets over-written). kSetKind :: Name -> Kind -> KindM () -- | The sub-computation is about the given range of the source code. kInRange :: Range -> KindM a -> KindM a kNewGoals :: ConstraintSource -> [Prop] -> KindM () kInInferM :: InferM a -> KindM a instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.Monad.InferOutput a) instance GHC.Show.Show Cryptol.TypeCheck.Monad.InferInput instance Control.DeepSeq.NFData Cryptol.TypeCheck.Monad.NameSeeds instance GHC.Generics.Generic Cryptol.TypeCheck.Monad.NameSeeds instance GHC.Show.Show Cryptol.TypeCheck.Monad.NameSeeds instance GHC.Base.Functor Cryptol.TypeCheck.Monad.KindM instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.KindM instance GHC.Base.Monad Cryptol.TypeCheck.Monad.KindM instance GHC.Base.Functor Cryptol.TypeCheck.Monad.InferM instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.InferM instance GHC.Base.Monad Cryptol.TypeCheck.Monad.InferM instance Control.Monad.Fix.MonadFix Cryptol.TypeCheck.Monad.InferM instance Cryptol.ModuleSystem.Name.FreshM Cryptol.TypeCheck.Monad.InferM module Cryptol.TypeCheck.Solver.Selector -- | Solve has-constraints. tryHasGoal :: HasGoal -> InferM (Bool, Bool) module Cryptol.TypeCheck.Sanity tcExpr :: InferInput -> Expr -> Either Error (Schema, [ProofObligation]) tcDecls :: InferInput -> [DeclGroup] -> Either Error [ProofObligation] tcModule :: InferInput -> Module -> Either Error [ProofObligation] type ProofObligation = Schema data Error -- | expected, actual TypeMismatch :: String -> Schema -> Schema -> Error -- | expected a mono type, got this ExpectedMono :: Schema -> Error TupleSelectorOutOfRange :: Int -> Int -> Error MissingField :: Ident -> [Ident] -> Error UnexpectedTupleShape :: Int -> Int -> Error UnexpectedRecordShape :: [Ident] -> [Ident] -> Error UnexpectedSequenceShape :: Int -> Type -> Error BadSelector :: Selector -> Type -> Error BadInstantiation :: Error Captured :: TVar -> Error BadProofNoAbs :: Error BadProofTyVars :: [TParam] -> Error KindMismatch :: Kind -> Kind -> Error NotEnoughArgumentsInKind :: Kind -> Error BadApplication :: Type -> Type -> Error FreeTypeVariable :: TVar -> Error BadTypeApplication :: Kind -> [Kind] -> Error RepeatedVariableInForall :: TParam -> Error BadMatch :: Type -> Error EmptyArm :: Error UndefinedTypeVaraible :: TVar -> Error UndefinedVariable :: Name -> Error same :: Same a => a -> a -> Bool instance GHC.Show.Show Cryptol.TypeCheck.Sanity.Error instance GHC.Base.Functor Cryptol.TypeCheck.Sanity.TcM instance GHC.Base.Applicative Cryptol.TypeCheck.Sanity.TcM instance GHC.Base.Monad Cryptol.TypeCheck.Sanity.TcM instance Cryptol.TypeCheck.Sanity.Same a => Cryptol.TypeCheck.Sanity.Same [a] instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.Type instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.Schema instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.TParam module Cryptol.TypeCheck.Instantiate instantiateWith :: Name -> Expr -> Schema -> [Located (Maybe Ident, Type)] -> InferM (Expr, Type) module Cryptol.TypeCheck.Depends data TyDecl -- | Type synonym TS :: (TySyn Name) -> (Maybe String) -> TyDecl -- | Newtype NT :: (Newtype Name) -> (Maybe String) -> TyDecl -- | Parameter type AT :: (ParameterType Name) -> (Maybe String) -> TyDecl -- | Property synonym PS :: (PropSyn Name) -> (Maybe String) -> TyDecl setDocString :: Maybe String -> TyDecl -> TyDecl -- | Check for duplicate and recursive type synonyms. Returns the -- type-synonyms in dependency order. orderTyDecls :: [TyDecl] -> InferM [TyDecl] -- | Associate type signatures with bindings and order bindings by -- dependency. orderBinds :: [Bind Name] -> [SCC (Bind Name)] class FromDecl d toBind :: FromDecl d => d -> Maybe (Bind Name) toParamFun :: FromDecl d => d -> Maybe (ParameterFun Name) toParamConstraints :: FromDecl d => d -> [Located (Prop Name)] toTyDecl :: FromDecl d => d -> Maybe TyDecl isTopDecl :: FromDecl d => d -> Bool -- | Given a list of declarations, annoted with (i) the names that they -- define, and (ii) the names that they use, we compute a list of -- strongly connected components of the declarations. The SCCs are in -- dependency order. mkScc :: [(a, [Name], [Name])] -> [SCC a] -- | Combine a bunch of definitions into a single map. Here we check that -- each name is defined only onces. combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a)) -- | Combine a bunch of definitions into a single map. Here we check that -- each name is defined only onces. combine :: [(Name, Located a)] -> InferM (Map Name (Located a)) -- | Identify multiple occurances of something. duplicates :: Ord a => [Located a] -> [(a, [Range])] instance Cryptol.TypeCheck.Depends.FromDecl (Cryptol.Parser.AST.TopDecl Cryptol.ModuleSystem.Name.Name) instance Cryptol.TypeCheck.Depends.FromDecl (Cryptol.Parser.AST.Decl Cryptol.ModuleSystem.Name.Name) module Cryptol.TypeCheck.Default -- | We default constraints of the form Literal t a to a := -- [width t] defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning]) improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning]) -- | Try to pick a reasonable instantiation for an expression with the -- given type. This is useful when we do evaluation at the REPL. The -- resulting types should satisfy the constraints of the schema. The -- parameters should be all of numeric kind, and the props should als be -- numeric defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)]) module Cryptol.TypeCheck.Solve simplifyAllConstraints :: InferM () -- | Prove an implication, and return any improvements that we computed. -- Records errors, if any of the goals couldn't be solved. proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst -- | Try to clean-up any left-over constraints after we've checked -- everything in a module. Typically these are either trivial things, or -- constraints on the module's type parameters. proveModuleTopLevel :: InferM () -- | Add additional constraints that ensure the validity of a type. wfType :: Type -> [Prop] -- | Add additional constraints that ensure validity of type function. Note -- that these constraints do not introduce additional malformed types, so -- the well-formedness constraints are guaranteed to be well-formed. This -- assumes that the parameters are well-formed. wfTypeFunction :: TFun -> [Type] -> [Prop] -- | Add additional constraints that ensure validity of a type constructor -- application. Note that the constraints do not use any partial type -- functions, so the new constraints are guaranteed to be well-formed. -- This assumes that the parameters are well-formed. wfTC :: TC -> [Type] -> [Prop] defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning]) defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr)) module Cryptol.TypeCheck.Kind checkType :: Type Name -> Maybe Kind -> InferM Type -- | Check a type signature. Returns validated schema, and any implicit -- constraints that we inferred. checkSchema :: AllowWildCards -> Schema Name -> InferM (Schema, [Goal]) -- | Check a newtype declaration. XXX: Do something with constraints. checkNewtype :: Newtype Name -> Maybe String -> InferM Newtype -- | Check a type-synonym declaration. checkTySyn :: TySyn Name -> Maybe String -> InferM TySyn -- | Check a constraint-synonym declaration. checkPropSyn :: PropSyn Name -> Maybe String -> InferM TySyn -- | Check a module parameter declarations. Nothing much to check, we just -- translate from one syntax to another. checkParameterType :: ParameterType Name -> Maybe String -> InferM ModTParam checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop] -- | Assumes that the NoPat pass has been run. module Cryptol.TypeCheck.Infer checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl inferModule :: Module Name -> InferM Module -- | inferBinds isTopLevel isRec binds performs inference for a -- strongly-connected component of Binds. If isTopLevel -- is true, any bindings without type signatures will be generalized. If -- it is false, and the mono-binds flag is enabled, no bindings without -- type signatures will be generalized, but bindings with signatures will -- be unaffected. inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl] inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a module Cryptol.TypeCheck.CheckModuleInstance -- | Check that the instance provides what the functor needs. checkModuleInstance :: Module -> Module -> InferM Module module Cryptol.TypeCheck tcModule :: Module Name -> InferInput -> IO (InferOutput Module) -- | Check a module instantiation, assuming that the functor has already -- been checked. tcModuleInst :: Module -> Module Name -> InferInput -> IO (InferOutput Module) tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema)) tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup]) -- | Information needed for type inference. data InferInput InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> !(Map Name ModTParam) -> !([Located Prop]) -> !(Map Name ModVParam) -> NameSeeds -> Bool -> SolverConfig -> [FilePath] -> !PrimMap -> !Supply -> InferInput -- | Location of program source [inpRange] :: InferInput -> Range -- | Variables that are in scope [inpVars] :: InferInput -> Map Name Schema -- | Type synonyms that are in scope [inpTSyns] :: InferInput -> Map Name TySyn -- | Newtypes in scope [inpNewtypes] :: InferInput -> Map Name Newtype -- | Type parameters [inpParamTypes] :: InferInput -> !(Map Name ModTParam) -- | Constraints on parameters [inpParamConstraints] :: InferInput -> !([Located Prop]) -- | Value parameters [inpParamFuns] :: InferInput -> !(Map Name ModVParam) -- | Private state of type-checker [inpNameSeeds] :: InferInput -> NameSeeds -- | Should local bindings without signatures be monomorphized? [inpMonoBinds] :: InferInput -> Bool -- | Options for the constraint solver [inpSolverConfig] :: InferInput -> SolverConfig -- | Where to look for Cryptol theory file. [inpSearchPath] :: InferInput -> [FilePath] -- | This is used when the type-checker needs to refer to a predefined -- identifier (e.g., number). [inpPrimNames] :: InferInput -> !PrimMap -- | The supply for fresh name generation [inpSupply] :: InferInput -> !Supply -- | The results of type inference. data InferOutput a -- | We found some errors InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a -- | Type inference was successful. InferOK :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a data SolverConfig SolverConfig :: FilePath -> [String] -> Int -> [FilePath] -> SolverConfig -- | The SMT solver to invoke [solverPath] :: SolverConfig -> FilePath -- | Additional arguments to pass to the solver [solverArgs] :: SolverConfig -> [String] -- | How verbose to be when type-checking [solverVerbose] :: SolverConfig -> Int -- | Look for the solver prelude in these locations. [solverPreludePath] :: SolverConfig -> [FilePath] -- | This is used for generating various names. data NameSeeds -- | The initial seeds, used when checking a fresh program. XXX: why does -- this start at 10? nameSeeds :: NameSeeds -- | Various errors that might happen during type checking/inference data Error -- | Just say this ErrorMsg :: Doc -> Error -- | Expected kind, inferred kind KindMismatch :: Kind -> Kind -> Error -- | Number of extra parameters, kind of result (which should not be of the -- form _ -> _) TooManyTypeParams :: Int -> Kind -> Error -- | A type variable was applied to some arguments. TyVarWithParams :: Error -- | Type-synonym, number of extra params TooManyTySynParams :: Name -> Int -> Error -- | Type-synonym, number of missing params TooFewTySynParams :: Name -> Int -> Error -- | The type synonym declarations are recursive RecursiveTypeDecls :: [Name] -> Error -- | Expected type, inferred type TypeMismatch :: Type -> Type -> Error -- | Unification results in a recursive type RecursiveType :: Type -> Type -> Error -- | A constraint that we could not solve The boolean indicates if we know -- that this constraint is impossible. UnsolvedGoals :: Bool -> [Goal] -> Error -- | A constraint (with context) that we could not solve UnsolvedDelayedCt :: DelayedCt -> Error -- | Type wild cards are not allowed in this context (e.g., definitions of -- type synonyms). UnexpectedTypeWildCard :: Error -- | Unification variable depends on quantified variables that are not in -- scope. TypeVariableEscaped :: Type -> [TParam] -> Error -- | Quantified type variables (of kind *) need to match the given type, so -- it does not work for all types. NotForAll :: TVar -> Type -> Error -- | The given constraints causes the signature of the function to be -- not-satisfiable. UnusableFunction :: Name -> [Prop] -> Error -- | Too many positional type arguments, in an explicit type instantiation TooManyPositionalTypeParams :: Error CannotMixPositionalAndNamedTypeParams :: Error UndefinedTypeParameter :: (Located Ident) -> Error RepeatedTypeParameter :: Ident -> [Range] -> Error AmbiguousType :: [Name] -> [TVar] -> Error data Warning DefaultingKind :: (TParam Name) -> Kind -> Warning DefaultingWildType :: Kind -> Warning DefaultingTo :: TVarInfo -> Type -> Warning ppWarning :: (Range, Warning) -> Doc ppError :: (Range, Error) -> Doc module Cryptol.ModuleSystem.Env -- | This is the current state of the interpreter. data ModuleEnv ModuleEnv :: LoadedModules -> NameSeeds -> SolverConfig -> EvalEnv -> CoreLint -> !Bool -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Supply -> ModuleEnv -- | Information about all loaded modules. See LoadedModule. -- Contains information such as the file where the module was loaded -- from, as well as the module's interface, used for type checking. [meLoadedModules] :: ModuleEnv -> LoadedModules -- | A source of new names for the type checker. [meNameSeeds] :: ModuleEnv -> NameSeeds -- | Configuration settings for the SMT solver used for type-checking. [meSolverConfig] :: ModuleEnv -> SolverConfig -- | The evaluation environment. Contains the values for all loaded -- modules, both public and private. [meEvalEnv] :: ModuleEnv -> EvalEnv -- | Should we run the linter to ensure sanity. [meCoreLint] :: ModuleEnv -> CoreLint -- | Are we assuming that local bindings are monomorphic. XXX: We should -- probably remove this flag, and set it to True. [meMonoBinds] :: ModuleEnv -> !Bool -- | The "current" module. Used to decide how to print names, for example. [meFocusedModule] :: ModuleEnv -> Maybe ModName -- | Where we look for things. [meSearchPath] :: ModuleEnv -> [FilePath] -- | This contains additional definitions that were made at the command -- line, and so they don't reside in any module. [meDynEnv] :: ModuleEnv -> DynamicEnv -- | Name source for the renamer [meSupply] :: ModuleEnv -> !Supply -- | Should we run the linter? data CoreLint -- | Don't run core lint NoCoreLint :: CoreLint -- | Run core lint CoreLint :: CoreLint resetModuleEnv :: ModuleEnv -> ModuleEnv initialModuleEnv :: IO ModuleEnv -- | Try to focus a loaded module in the module environment. focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv -- | Get a list of all the loaded modules. Each module in the resulting -- list depends only on other modules that precede it. loadedModules :: ModuleEnv -> [Module] -- | Produce an ifaceDecls that represents the focused environment of the -- module system, as well as a NameDisp for pretty-printing names -- according to the imports. -- -- XXX This could really do with some better error handling, just -- returning mempty when one of the imports fails isn't really desirable. -- -- XXX: This is not quite right. For example, it does not take into -- account *how* things were imported in a module (e.g., qualified). It -- would be simpler to simply store the naming environment that was -- actually used when we renamed the module. focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp) -- | The unqualified declarations and name environment for the dynamic -- environment. dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp) data LoadedModules LoadedModules :: [LoadedModule] -> [LoadedModule] -> LoadedModules -- | Invariants: 1) All the dependencies of any module m must -- precede m in the list. 2) Does not contain any parameterized -- modules. [lmLoadedModules] :: LoadedModules -> [LoadedModule] -- | Loaded parameterized modules. [lmLoadedParamModules] :: LoadedModules -> [LoadedModule] getLoadedModules :: LoadedModules -> [LoadedModule] data LoadedModule LoadedModule :: ModName -> FilePath -> FilePath -> Iface -> Module -> LoadedModule [lmName] :: LoadedModule -> ModName -- | The file path used to load this module (may not be canonical) [lmFilePath] :: LoadedModule -> FilePath -- | The canonical version of the path of this module [lmCanonicalPath] :: LoadedModule -> FilePath [lmInterface] :: LoadedModule -> Iface [lmModule] :: LoadedModule -> Module -- | Has this module been loaded already. isLoaded :: ModName -> LoadedModules -> Bool -- | Try to find a previously loaded module lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule -- | Add a freshly loaded module. If it was previously loaded, then the new -- version is ignored. addLoadedModule :: FilePath -> FilePath -> Module -> LoadedModules -> LoadedModules -- | Remove a previously loaded module. removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules -- | Extra information we need to carry around to dynamically extend an -- environment outside the context of a single module. Particularly -- useful when dealing with interactive declarations as in :let -- or it. data DynamicEnv DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv [deNames] :: DynamicEnv -> NamingEnv [deDecls] :: DynamicEnv -> [DeclGroup] [deEnv] :: DynamicEnv -> EvalEnv -- | Build IfaceDecls that correspond to all of the bindings in the -- dynamic environment. -- -- XXX: if we ever add type synonyms or newtypes at the REPL, revisit -- this. deIfaceDecls :: DynamicEnv -> IfaceDecls instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.ModuleEnv instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.DynamicEnv instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.DynamicEnv instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModules instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModules instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModules instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModule instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModule instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModule instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.CoreLint instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.CoreLint instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.ModuleEnv instance GHC.Base.Semigroup Cryptol.ModuleSystem.Env.DynamicEnv instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.DynamicEnv instance GHC.Base.Semigroup Cryptol.ModuleSystem.Env.LoadedModules instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.LoadedModules module Cryptol.Version commitHash :: String commitShortHash :: String commitBranch :: String commitDirty :: Bool version :: Version module Cryptol.Parser parseModule :: Config -> Text -> Either ParseError (Module PName) parseProgram :: Layout -> Text -> Either ParseError (Program PName) parseProgramWith :: Config -> Text -> Either ParseError (Program PName) parseExpr :: Text -> Either ParseError (Expr PName) parseExprWith :: Config -> Text -> Either ParseError (Expr PName) parseDecl :: Text -> Either ParseError (Decl PName) parseDeclWith :: Config -> Text -> Either ParseError (Decl PName) parseDecls :: Text -> Either ParseError [Decl PName] parseDeclsWith :: Config -> Text -> Either ParseError [Decl PName] parseLetDecl :: Text -> Either ParseError (Decl PName) parseLetDeclWith :: Config -> Text -> Either ParseError (Decl PName) parseRepl :: Text -> Either ParseError (ReplInput PName) parseReplWith :: Config -> Text -> Either ParseError (ReplInput PName) parseSchema :: Text -> Either ParseError (Schema PName) parseSchemaWith :: Config -> Text -> Either ParseError (Schema PName) parseModName :: String -> Maybe ModName parseHelpName :: String -> Maybe PName data ParseError HappyError :: FilePath -> (Located Token) -> ParseError HappyErrorMsg :: Range -> String -> ParseError HappyUnexpected :: FilePath -> (Maybe (Located Token)) -> String -> ParseError HappyOutOfTokens :: FilePath -> Position -> ParseError ppError :: ParseError -> Doc data Layout Layout :: Layout NoLayout :: Layout data Config Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config -- | File that we are working on [cfgSource] :: Config -> !FilePath -- | Settings for layout processing [cfgLayout] :: Config -> !Layout -- | Preprocessor settings [cfgPreProc] :: Config -> PreProc -- | Implicit includes [cfgAutoInclude] :: Config -> [FilePath] -- | When we do layout processing should we add a vCurly (i.e., are we -- parsing a list of things). [cfgModuleScope] :: Config -> Bool defaultConfig :: Config guessPreProc :: FilePath -> PreProc data PreProc None :: PreProc Markdown :: PreProc LaTeX :: PreProc module Cryptol.Parser.NoInclude removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName)) data IncludeError IncludeFailed :: (Located FilePath) -> IncludeError IncludeParseError :: ParseError -> IncludeError IncludeCycle :: [Located FilePath] -> IncludeError ppIncludeError :: IncludeError -> Doc instance Control.DeepSeq.NFData Cryptol.Parser.NoInclude.IncludeError instance GHC.Generics.Generic Cryptol.Parser.NoInclude.IncludeError instance GHC.Show.Show Cryptol.Parser.NoInclude.IncludeError instance GHC.Base.Functor Cryptol.Parser.NoInclude.NoIncM instance GHC.Base.Applicative Cryptol.Parser.NoInclude.NoIncM instance GHC.Base.Monad Cryptol.Parser.NoInclude.NoIncM module Cryptol.ModuleSystem.Monad data ImportSource FromModule :: ModName -> ImportSource FromImport :: (Located Import) -> ImportSource FromModuleInstance :: (Located ModName) -> ImportSource importedModule :: ImportSource -> ModName data ModuleError -- | Unable to find the module given, tried looking in these paths ModuleNotFound :: ModName -> [FilePath] -> ModuleError -- | Unable to open a file CantFindFile :: FilePath -> ModuleError -- | Some other IO error occurred while reading this file OtherIOError :: FilePath -> IOException -> ModuleError -- | Generated this parse error when parsing the file for module m ModuleParseError :: FilePath -> ParseError -> ModuleError -- | Recursive module group discovered RecursiveModules :: [ImportSource] -> ModuleError -- | Problems during the renaming phase RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError -- | Problems during the NoPat phase NoPatErrors :: ImportSource -> [Error] -> ModuleError -- | Problems during the NoInclude phase NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError -- | Problems during type checking TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError -- | Problems after type checking, eg. specialization OtherFailure :: String -> ModuleError -- | Module loaded by 'import' statement has the wrong module name ModuleNameMismatch :: ModName -> (Located ModName) -> ModuleError -- | Two modules loaded from different files have the same module name DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError -- | Attempt to import a parametrized module that was not instantiated. ImportedParamModule :: ModName -> ModuleError -- | Failed to add the module parameters to all definitions in a module. FailedToParameterizeModDefs :: ModName -> [Name] -> ModuleError NotAParameterizedModule :: ModName -> ModuleError -- | This is just a tag on the error, indicating the file containing it. It -- is convenient when we had to look for the module, and we'd like to -- communicate the location of pthe problematic module to the handler. ErrorInFile :: FilePath -> ModuleError -> ModuleError moduleNotFound :: ModName -> [FilePath] -> ModuleM a cantFindFile :: FilePath -> ModuleM a otherIOError :: FilePath -> IOException -> ModuleM a moduleParseError :: FilePath -> ParseError -> ModuleM a recursiveModules :: [ImportSource] -> ModuleM a renamerErrors :: [RenamerError] -> ModuleM a noPatErrors :: [Error] -> ModuleM a noIncludeErrors :: [IncludeError] -> ModuleM a typeCheckingFailed :: [(Range, Error)] -> ModuleM a moduleNameMismatch :: ModName -> Located ModName -> ModuleM a duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a importParamModule :: ModName -> ModuleM a failedToParameterizeModDefs :: ModName -> [Name] -> ModuleM a notAParameterizedModule :: ModName -> ModuleM a -- | Run the computation, and if it caused and error, tag the error with -- the given file. errorInFile :: FilePath -> ModuleM a -> ModuleM a data ModuleWarning TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning RenamerWarnings :: [RenamerWarning] -> ModuleWarning warn :: [ModuleWarning] -> ModuleM () typeCheckWarnings :: [(Range, Warning)] -> ModuleM () renamerWarnings :: [RenamerWarning] -> ModuleM () data RO RO :: [ImportSource] -> EvalOpts -> RO [roLoading] :: RO -> [ImportSource] [roEvalOpts] :: RO -> EvalOpts emptyRO :: EvalOpts -> RO newtype ModuleT m a ModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a -> ModuleT m a [unModuleT] :: ModuleT m a -> ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a runModuleT :: Monad m => (EvalOpts, ModuleEnv) -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning]) type ModuleM = ModuleT IO runModuleM :: (EvalOpts, ModuleEnv) -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning]) io :: BaseM m IO => IO a -> ModuleT m a getModuleEnv :: Monad m => ModuleT m ModuleEnv setModuleEnv :: Monad m => ModuleEnv -> ModuleT m () modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m () getLoadedMaybe :: ModName -> ModuleM (Maybe LoadedModule) isLoaded :: ModName -> ModuleM Bool loadingImport :: Located Import -> ModuleM a -> ModuleM a loadingModule :: ModName -> ModuleM a -> ModuleM a loadingModInstance :: Located ModName -> ModuleM a -> ModuleM a -- | Push an "interactive" context onto the loading stack. A bit of a hack, -- as it uses a faked module name interactive :: ModuleM a -> ModuleM a loading :: ImportSource -> ModuleM a -> ModuleM a -- | Get the currently focused import source. getImportSource :: ModuleM ImportSource getIface :: ModName -> ModuleM Iface getLoaded :: ModName -> ModuleM Module getNameSeeds :: ModuleM NameSeeds getSupply :: ModuleM Supply getMonoBinds :: ModuleM Bool setMonoBinds :: Bool -> ModuleM () setNameSeeds :: NameSeeds -> ModuleM () setSupply :: Supply -> ModuleM () unloadModule :: (LoadedModule -> Bool) -> ModuleM () loadedModule :: FilePath -> FilePath -> Module -> ModuleM () modifyEvalEnv :: (EvalEnv -> Eval EvalEnv) -> ModuleM () getEvalEnv :: ModuleM EvalEnv getEvalOpts :: ModuleM EvalOpts getFocusedModule :: ModuleM (Maybe ModName) setFocusedModule :: ModName -> ModuleM () getSearchPath :: ModuleM [FilePath] -- | Run a ModuleM action in a context with a prepended search path. -- Useful for temporarily looking in other places while resolving -- imports, for example. withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a getFocusedEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv, NameDisp) getDynEnv :: ModuleM DynamicEnv setDynEnv :: DynamicEnv -> ModuleM () setSolver :: SolverConfig -> ModuleM () getSolverConfig :: ModuleM SolverConfig -- | Usefule for logging. For example: withLogger logPutStrLn -- Hello withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleWarning instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ModuleWarning instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleWarning instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleError instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ImportSource instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ImportSource instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ImportSource instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Monad.ModuleT m) instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Monad.ModuleT m) instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Monad.ModuleT m) instance MonadLib.MonadT Cryptol.ModuleSystem.Monad.ModuleT instance GHC.Base.Monad m => Cryptol.ModuleSystem.Name.FreshM (Cryptol.ModuleSystem.Monad.ModuleT m) instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Cryptol.ModuleSystem.Monad.ModuleT m) instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleWarning instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleError instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleError instance GHC.Classes.Eq Cryptol.ModuleSystem.Monad.ImportSource instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ImportSource -- | This is the main driver---it provides entry points for the various -- passes. module Cryptol.ModuleSystem.Base rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a -- | Rename a module in the context of its imported modules. renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name) -- | Run the noPat pass. noPat :: RemovePatterns a => a -> ModuleM a parseModule :: FilePath -> ModuleM (Module PName) -- | Load a module by its path. loadModuleByPath :: FilePath -> ModuleM Module -- | Load a module, unless it was previously loaded. loadModuleFrom :: ImportSource -> ModuleM (FilePath, Module) -- | Load dependencies, typecheck, and add to the eval environment. doLoadModule :: ImportSource -> FilePath -> Module PName -> ModuleM Module -- | Rewrite an import declaration to be of the form: -- -- 
--   import foo as foo [ [hiding] (a,b,c) ]
--
fullyQualified :: Import -> Import -- | Find the interface referenced by an import, and generate the naming -- environment that it describes. importIface :: Import -> ModuleM (IfaceDecls, NamingEnv) -- | Load a series of interfaces, merging their public interfaces. importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv) moduleFile :: ModName -> String -> FilePath -- | Discover a module. findModule :: ModName -> ModuleM FilePath -- | Discover a file. This is distinct from findModule in that we -- assume we've already been given a particular file name. findFile :: FilePath -> ModuleM FilePath -- | Add the prelude to the import list if it's not already mentioned. addPrelude :: Module PName -> Module PName -- | Load the dependencies of a module into the environment. loadDeps :: Module name -> ModuleM () -- | Load the local environment, which consists of the environment for the -- currently opened module, shadowed by the dynamic environment. getLocalEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv) -- | Typecheck a single expression, yielding a renamed parsed expression, -- typechecked core expression, and a type schema. checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema) -- | Typecheck a group of declarations. -- -- INVARIANT: This assumes that NoPat has already been run on the -- declarations. checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup]) -- | Generate the primitive map. If the prelude is currently being loaded, -- this should be generated directly from the naming environment given to -- the renamer instead. getPrimMap :: ModuleM PrimMap -- | Load a module, be it a normal module or a functor instantiation. checkModule :: ImportSource -> FilePath -> Module PName -> ModuleM Module -- | Typecheck a single module. If the module is an instantiation of a -- functor, then this just type-checks the instantiating parameters. See -- checkModule checkSingleModule :: Act (Module Name) Module -> ImportSource -> FilePath -> Module PName -> ModuleM Module data TCLinter o TCLinter :: o -> InferInput -> Either Error [ProofObligation] -> Maybe ModName -> TCLinter o [lintCheck] :: TCLinter o -> o -> InferInput -> Either Error [ProofObligation] [lintModule] :: TCLinter o -> Maybe ModName exprLinter :: TCLinter (Expr, Schema) declsLinter :: TCLinter [DeclGroup] moduleLinter :: ModName -> TCLinter Module type Act i o = i -> InferInput -> IO (InferOutput o) data TCAction i o TCAction :: Act i o -> TCLinter o -> PrimMap -> TCAction i o [tcAction] :: TCAction i o -> Act i o [tcLinter] :: TCAction i o -> TCLinter o [tcPrims] :: TCAction i o -> PrimMap typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o -- | Generate input for the typechecker. genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput evalExpr :: Expr -> ModuleM Value evalDecls :: [DeclGroup] -> ModuleM () module Cryptol.ModuleSystem -- | This is the current state of the interpreter. data ModuleEnv ModuleEnv :: LoadedModules -> NameSeeds -> SolverConfig -> EvalEnv -> CoreLint -> !Bool -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Supply -> ModuleEnv -- | Information about all loaded modules. See LoadedModule. -- Contains information such as the file where the module was loaded -- from, as well as the module's interface, used for type checking. [meLoadedModules] :: ModuleEnv -> LoadedModules -- | A source of new names for the type checker. [meNameSeeds] :: ModuleEnv -> NameSeeds -- | Configuration settings for the SMT solver used for type-checking. [meSolverConfig] :: ModuleEnv -> SolverConfig -- | The evaluation environment. Contains the values for all loaded -- modules, both public and private. [meEvalEnv] :: ModuleEnv -> EvalEnv -- | Should we run the linter to ensure sanity. [meCoreLint] :: ModuleEnv -> CoreLint -- | Are we assuming that local bindings are monomorphic. XXX: We should -- probably remove this flag, and set it to True. [meMonoBinds] :: ModuleEnv -> !Bool -- | The "current" module. Used to decide how to print names, for example. [meFocusedModule] :: ModuleEnv -> Maybe ModName -- | Where we look for things. [meSearchPath] :: ModuleEnv -> [FilePath] -- | This contains additional definitions that were made at the command -- line, and so they don't reside in any module. [meDynEnv] :: ModuleEnv -> DynamicEnv -- | Name source for the renamer [meSupply] :: ModuleEnv -> !Supply initialModuleEnv :: IO ModuleEnv -- | Extra information we need to carry around to dynamically extend an -- environment outside the context of a single module. Particularly -- useful when dealing with interactive declarations as in :let -- or it. data DynamicEnv DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv [deNames] :: DynamicEnv -> NamingEnv [deDecls] :: DynamicEnv -> [DeclGroup] [deEnv] :: DynamicEnv -> EvalEnv data ModuleError -- | Unable to find the module given, tried looking in these paths ModuleNotFound :: ModName -> [FilePath] -> ModuleError -- | Unable to open a file CantFindFile :: FilePath -> ModuleError -- | Some other IO error occurred while reading this file OtherIOError :: FilePath -> IOException -> ModuleError -- | Generated this parse error when parsing the file for module m ModuleParseError :: FilePath -> ParseError -> ModuleError -- | Recursive module group discovered RecursiveModules :: [ImportSource] -> ModuleError -- | Problems during the renaming phase RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError -- | Problems during the NoPat phase NoPatErrors :: ImportSource -> [Error] -> ModuleError -- | Problems during the NoInclude phase NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError -- | Problems during type checking TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError -- | Problems after type checking, eg. specialization OtherFailure :: String -> ModuleError -- | Module loaded by 'import' statement has the wrong module name ModuleNameMismatch :: ModName -> (Located ModName) -> ModuleError -- | Two modules loaded from different files have the same module name DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError -- | Attempt to import a parametrized module that was not instantiated. ImportedParamModule :: ModName -> ModuleError -- | Failed to add the module parameters to all definitions in a module. FailedToParameterizeModDefs :: ModName -> [Name] -> ModuleError NotAParameterizedModule :: ModName -> ModuleError -- | This is just a tag on the error, indicating the file containing it. It -- is convenient when we had to look for the module, and we'd like to -- communicate the location of pthe problematic module to the handler. ErrorInFile :: FilePath -> ModuleError -> ModuleError data ModuleWarning TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning RenamerWarnings :: [RenamerWarning] -> ModuleWarning type ModuleCmd a = (EvalOpts, ModuleEnv) -> IO (ModuleRes a) type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) -- | Find the file associated with a module name in the module search path. findModule :: ModName -> ModuleCmd FilePath -- | Load the module contained in the given file. loadModuleByPath :: FilePath -> ModuleCmd (FilePath, Module) -- | Load the given parsed module. loadModuleByName :: ModName -> ModuleCmd (FilePath, Module) -- | Check the type of an expression. Give back the renamed expression, the -- core expression, and its type schema. checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema) -- | Evaluate an expression. evalExpr :: Expr -> ModuleCmd Value -- | Typecheck top-level declarations. checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup]) -- | Evaluate declarations and add them to the extended environment. evalDecls :: [DeclGroup] -> ModuleCmd () noPat :: RemovePatterns a => a -> ModuleCmd a -- | Produce an ifaceDecls that represents the focused environment of the -- module system, as well as a NameDisp for pretty-printing names -- according to the imports. -- -- XXX This could really do with some better error handling, just -- returning mempty when one of the imports fails isn't really desirable. -- -- XXX: This is not quite right. For example, it does not take into -- account *how* things were imported in a module (e.g., qualified). It -- would be simpler to simply store the naming environment that was -- actually used when we renamed the module. focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp) getPrimMap :: ModuleCmd PrimMap renameVar :: NamingEnv -> PName -> ModuleCmd Name renameType :: NamingEnv -> PName -> ModuleCmd Name -- | The resulting interface generated by a module that has been -- typechecked. data Iface Iface :: !ModName -> IfaceDecls -> IfaceDecls -> IfaceParams -> Iface -- | Module name [ifModName] :: Iface -> !ModName -- | Exported definitions [ifPublic] :: Iface -> IfaceDecls -- | Private defintiions [ifPrivate] :: Iface -> IfaceDecls -- | Uninterpreted constants (aka module params) [ifParams] :: Iface -> IfaceParams data IfaceParams IfaceParams :: Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> IfaceParams [ifParamTypes] :: IfaceParams -> Map Name ModTParam -- | Constraints on param. types [ifParamConstraints] :: IfaceParams -> [Located Prop] [ifParamFuns] :: IfaceParams -> Map Name ModVParam data IfaceDecls IfaceDecls :: Map Name IfaceTySyn -> Map Name IfaceNewtype -> Map Name IfaceDecl -> IfaceDecls [ifTySyns] :: IfaceDecls -> Map Name IfaceTySyn [ifNewtypes] :: IfaceDecls -> Map Name IfaceNewtype [ifDecls] :: IfaceDecls -> Map Name IfaceDecl -- | Generate an Iface from a typechecked module. genIface :: Module -> Iface type IfaceTySyn = TySyn data IfaceDecl IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl -- | Name of thing [ifDeclName] :: IfaceDecl -> !Name -- | Type [ifDeclSig] :: IfaceDecl -> Schema -- | Pragmas [ifDeclPragmas] :: IfaceDecl -> [Pragma] -- | Is this an infix thing [ifDeclInfix] :: IfaceDecl -> Bool -- | Fixity information [ifDeclFixity] :: IfaceDecl -> Maybe Fixity -- | Documentation [ifDeclDoc] :: IfaceDecl -> Maybe String module Cryptol.Transform.Specialize -- | A Name should have an entry in the SpecCache iff it is specializable. -- Each Name starts out with an empty TypesMap. type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl)) -- | The specializer monad. type SpecT m a = StateT SpecCache (ModuleT m) a type SpecM a = SpecT IO a runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache) liftSpecT :: Monad m => ModuleT m a -> SpecT m a getSpecCache :: Monad m => SpecT m SpecCache setSpecCache :: Monad m => SpecCache -> SpecT m () modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m () modify :: StateM m s => (s -> s) -> m () -- | Add a `where` clause to the given expression containing -- type-specialized versions of all functions called (transitively) by -- the body of the expression. specialize :: Expr -> ModuleCmd Expr specializeExpr :: Expr -> SpecM Expr specializeMatch :: Match -> SpecM Match -- | Add the declarations to the SpecCache, run the given monadic action, -- and then pull the specialized declarations back out of the SpecCache -- state. Return the result along with the declarations and a table of -- names of specialized bindings. withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name)) -- | Compute the specialization of `EWhere e dgs`. A decl within -- dgs is replicated once for each monomorphic type instance at -- which it is used; decls not mentioned in e (even monomorphic -- ones) are simply dropped. specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr -- | Transform the given declaration groups into a set of monomorphic -- declarations. All of the original declarations with monomorphic types -- are kept; additionally the result set includes instantiated versions -- of polymorphic decls that are referenced by the monomorphic bindings. -- We also return a map relating generated names to the names from the -- original declarations. specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name)) specializeConst :: Expr -> SpecM Expr destEProofApps :: Expr -> (Expr, Int) destETApps :: Expr -> (Expr, [Type]) destEProofAbs :: Expr -> ([Prop], Expr) destETAbs :: Expr -> ([TParam], Expr) -- | Freshen a name by giving it a new unique. freshName :: Name -> [Type] -> SpecM Name instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema -- | Reduce `length ts` outermost type abstractions and n proof -- abstractions. instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr allDeclGroups :: ModuleEnv -> [DeclGroup] allLoadedModules :: ModuleEnv -> [LoadedModule] allPublicNames :: ModuleEnv -> [Name] traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c) module Cryptol.Symbolic type EvalEnv = GenEvalEnv SBool SWord proverConfigs :: [(String, SMTConfig)] proverNames :: [String] lookupProver :: String -> SMTConfig type SatResult = [(Type, Expr, Value)] data SatNum AllSat :: SatNum SomeSat :: Int -> SatNum data QueryType SatQuery :: SatNum -> QueryType ProveQuery :: QueryType data ProverCommand ProverCommand :: QueryType -> String -> Bool -> !(IORef ProverStats) -> [DeclGroup] -> Maybe FilePath -> Expr -> Schema -> ProverCommand -- | The type of query to run [pcQueryType] :: ProverCommand -> QueryType -- | Which prover to use (one of the strings in proverConfigs) [pcProverName] :: ProverCommand -> String -- | Verbosity flag passed to SBV [pcVerbose] :: ProverCommand -> Bool -- | Record timing information here [pcProverStats] :: ProverCommand -> !(IORef ProverStats) -- | Extra declarations to bring into scope for symbolic simulation [pcExtraDecls] :: ProverCommand -> [DeclGroup] -- | Optionally output the SMTLIB query to a file [pcSmtFile] :: ProverCommand -> Maybe FilePath -- | The typechecked expression to evaluate [pcExpr] :: ProverCommand -> Expr -- | The Schema of pcExpr [pcSchema] :: ProverCommand -> Schema type ProverStats = NominalDiffTime -- | A prover result is either an error message, an empty result (eg for -- the offline prover), a counterexample or a lazy list of satisfying -- assignments. data ProverResult AllSatResult :: [SatResult] -> ProverResult ThmResult :: [Type] -> ProverResult EmptyResult :: ProverResult ProverError :: String -> ProverResult satSMTResults :: SatResult -> [SMTResult] allSatSMTResults :: AllSatResult -> [SMTResult] thmSMTResults :: ThmResult -> [SMTResult] proverError :: String -> ModuleCmd (Maybe Solver, ProverResult) satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult) satProveOffline :: ProverCommand -> ModuleCmd (Either String String) protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a parseValues :: [FinType] -> [CW] -> ([Value], [CW]) parseValue :: FinType -> [CW] -> (Value, [CW]) allDeclGroups :: ModuleEnv -> [DeclGroup] data FinType FTBit :: FinType FTInteger :: FinType FTIntMod :: Integer -> FinType FTSeq :: Int -> FinType -> FinType FTTuple :: [FinType] -> FinType FTRecord :: [(Ident, FinType)] -> FinType numType :: Integer -> Maybe Int finType :: TValue -> Maybe FinType unFinType :: FinType -> Type predArgTypes :: Schema -> Either String [FinType] inBoundsIntMod :: Integer -> SInteger -> SBool forallFinType :: FinType -> WriterT [SBool] Symbolic Value existsFinType :: FinType -> WriterT [SBool] Symbolic Value instance GHC.Show.Show Cryptol.Symbolic.QueryType instance GHC.Show.Show Cryptol.Symbolic.SatNum module Cryptol.REPL.Monad -- | REPL_ context with InputT handling. newtype REPL a REPL :: IORef RW -> IO a -> REPL a [unREPL] :: REPL a -> IORef RW -> IO a -- | Run a REPL action with a fresh environment. runREPL :: Bool -> Logger -> REPL a -> IO a io :: IO a -> REPL a -- | Raise an exception. raise :: REPLException -> REPL a stop :: REPL () catch :: REPL a -> (REPLException -> REPL a) -> REPL a -- | Use the configured output action to print a string with a trailing -- newline rPutStrLn :: String -> REPL () -- | Use the configured output action to print a string rPutStr :: String -> REPL () -- | Use the configured output action to print something using its Show -- instance rPrint :: Show a => a -> REPL () -- | REPL exceptions. data REPLException ParseError :: ParseError -> REPLException FileNotFound :: FilePath -> REPLException DirectoryNotFound :: FilePath -> REPLException NoPatError :: [Error] -> REPLException NoIncludeError :: [IncludeError] -> REPLException EvalError :: EvalError -> REPLException ModuleSystemError :: NameDisp -> ModuleError -> REPLException EvalPolyError :: Schema -> REPLException TypeNotTestable :: Type -> REPLException EvalInParamModule :: ModName -> [Name] -> REPLException SBVError :: String -> REPLException rethrowEvalError :: IO a -> IO a getFocusedEnv :: REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp) getModuleEnv :: REPL ModuleEnv setModuleEnv :: ModuleEnv -> REPL () getDynEnv :: REPL DynamicEnv setDynEnv :: DynamicEnv -> REPL () -- | Given an existing qualified name, prefix it with a relatively-unique -- string. We make it unique by prefixing with a character # -- that is not lexically valid in a module name. uniqify :: Name -> REPL Name -- | Generate a fresh name using the given index. The name will reside -- within the "interactive" namespace. freshName :: Ident -> NameSource -> REPL Name getTSyns :: REPL (Map Name TySyn) getNewtypes :: REPL (Map Name Newtype) getVars :: REPL (Map Name IfaceDecl) whenDebug :: REPL () -> REPL () -- | Get visible variable names. getExprNames :: REPL [String] -- | Get visible type signature names. getTypeNames :: REPL [String] -- | Return a list of property names, sorted by position in the file. getPropertyNames :: REPL ([Name], NameDisp) getModNames :: REPL [ModName] -- | This indicates what the user would like to work on. data LoadedModule LoadedModule :: Maybe ModName -> FilePath -> LoadedModule -- | Working on this module. [lName] :: LoadedModule -> Maybe ModName -- | Working on this file. [lPath] :: LoadedModule -> FilePath getLoadedMod :: REPL (Maybe LoadedModule) -- | Set the name of the currently focused file, edited by :e and -- loaded via :r. setLoadedMod :: LoadedModule -> REPL () clearLoadedMod :: REPL () setEditPath :: FilePath -> REPL () setSearchPath :: [FilePath] -> REPL () prependSearchPath :: [FilePath] -> REPL () -- | Construct the prompt for the current environment. getPrompt :: REPL String shouldContinue :: REPL Bool unlessBatch :: REPL () -> REPL () -- | Run a computation in batch mode, restoring the previous isBatch flag -- afterwards asBatch :: REPL a -> REPL a disableLet :: REPL () enableLet :: REPL () -- | Are let-bindings enabled in this REPL? getLetEnabled :: REPL Bool -- | Is evaluation enabled. If the currently focused module is -- parameterized, then we cannot evalute. validEvalContext :: FreeVars a => a -> REPL () -- | Update the title updateREPLTitle :: REPL () -- | Set the function that will be called when updating the title setUpdateREPLTitle :: REPL () -> REPL () data EnvVal EnvString :: String -> EnvVal EnvProg :: String -> [String] -> EnvVal EnvNum :: !Int -> EnvVal EnvBool :: Bool -> EnvVal data OptionDescr OptionDescr :: String -> EnvVal -> Checker -> String -> EnvVal -> REPL () -> OptionDescr [optName] :: OptionDescr -> String [optDefault] :: OptionDescr -> EnvVal [optCheck] :: OptionDescr -> Checker [optHelp] :: OptionDescr -> String [optEff] :: OptionDescr -> EnvVal -> REPL () -- | Set a user option. setUser :: String -> String -> REPL () -- | Get a user option, when it's known to exist. Fail with panic when it -- doesn't. getUser :: String -> REPL EnvVal -- | Get a user option, using Maybe for failure. tryGetUser :: String -> REPL (Maybe EnvVal) userOptions :: OptionMap getUserSatNum :: REPL SatNum getUserShowProverStats :: REPL Bool -- | Get the REPL's string-printer getPutStr :: REPL (String -> IO ()) getLogger :: REPL Logger -- | Set the REPL's string-printer setPutStr :: (String -> IO ()) -> REPL () smokeTest :: REPL [Smoke] data Smoke Z3NotFound :: Smoke instance GHC.Classes.Eq Cryptol.REPL.Monad.Smoke instance GHC.Show.Show Cryptol.REPL.Monad.Smoke instance GHC.Show.Show Cryptol.REPL.Monad.EnvVal instance GHC.Show.Show Cryptol.REPL.Monad.REPLException instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.Smoke instance GHC.Base.Functor Cryptol.REPL.Monad.REPL instance GHC.Base.Applicative Cryptol.REPL.Monad.REPL instance GHC.Base.Monad Cryptol.REPL.Monad.REPL instance Control.Monad.IO.Class.MonadIO Cryptol.REPL.Monad.REPL instance Control.Monad.Base.MonadBase GHC.Types.IO Cryptol.REPL.Monad.REPL instance Control.Monad.Trans.Control.MonadBaseControl GHC.Types.IO Cryptol.REPL.Monad.REPL instance Cryptol.ModuleSystem.Name.FreshM Cryptol.REPL.Monad.REPL instance GHC.Exception.Exception Cryptol.REPL.Monad.REPLException instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.REPLException module Cryptol.Eval.Reference -- | Value type for the reference evaluator. data Value -- | Bit booleans VBit :: (Either EvalError Bool) -> Value -- | Integer integers VInteger :: (Either EvalError Integer) -> Value -- | [n]a finite or infinite lists VList :: Nat' -> [Value] -> Value -- | ( .. ) tuples VTuple :: [Value] -> Value -- | { .. } records VRecord :: [(Ident, Value)] -> Value -- | functions VFun :: (Value -> Value) -> Value -- | polymorphic values (kind *) VPoly :: (TValue -> Value) -> Value -- | polymorphic values (kind #) VNumPoly :: (Nat' -> Value) -> Value evaluate :: Expr -> ModuleCmd Value ppValue :: PPOpts -> Value -> Doc instance GHC.Base.Semigroup Cryptol.Eval.Reference.Env instance GHC.Base.Monoid Cryptol.Eval.Reference.Env module Cryptol.REPL.Command -- | Commands. data Command -- | Successfully parsed command Command :: (REPL ()) -> Command -- | Ambiguous command, list of conflicting commands Ambiguous :: String -> [String] -> Command -- | The unknown command Unknown :: String -> Command -- | Command builder. data CommandDescr CommandDescr :: [String] -> CommandBody -> String -> CommandDescr [cNames] :: CommandDescr -> [String] [cBody] :: CommandDescr -> CommandBody [cHelp] :: CommandDescr -> String data CommandBody ExprArg :: (String -> REPL ()) -> CommandBody FileExprArg :: (FilePath -> String -> REPL ()) -> CommandBody DeclsArg :: (String -> REPL ()) -> CommandBody ExprTypeArg :: (String -> REPL ()) -> CommandBody ModNameArg :: (String -> REPL ()) -> CommandBody FilenameArg :: (FilePath -> REPL ()) -> CommandBody OptionArg :: (String -> REPL ()) -> CommandBody ShellArg :: (String -> REPL ()) -> CommandBody HelpArg :: (String -> REPL ()) -> CommandBody NoArg :: (REPL ()) -> CommandBody data CommandExitCode CommandOk :: CommandExitCode CommandError :: CommandExitCode -- | Parse a line as a command. parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command -- | Run a command. runCommand :: Command -> REPL CommandExitCode -- | Split at the first word boundary. splitCommand :: String -> Maybe (String, String) -- | Lookup a string in the command list. findCommand :: String -> [CommandDescr] -- | Lookup a string in the command list, returning an exact match even if -- it's the prefix of another command. findCommandExact :: String -> [CommandDescr] -- | Lookup a string in the notebook-safe command list. findNbCommand :: Bool -> String -> [CommandDescr] moduleCmd :: String -> REPL () loadCmd :: FilePath -> REPL () loadPrelude :: REPL () setOptionCmd :: String -> REPL () interactiveConfig :: Config replParseExpr :: String -> REPL (Expr PName) replEvalExpr :: Expr PName -> REPL (Value, Type) replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema) -- | Randomly test a property, or exhaustively check it if the number of -- values in the type under test is smaller than the tests -- environment variable, or we specify exhaustive testing. qcCmd :: QCMode -> String -> REPL [TestReport] data QCMode QCRandom :: QCMode QCExhaust :: QCMode satCmd :: String -> REPL () proveCmd :: String -> REPL () onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats) offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String) handleCtrlC :: a -> REPL a -- | Strip leading space. sanitize :: String -> String -- | Lift a parsing action into the REPL monad. replParse :: (String -> Either ParseError a) -> String -> REPL a liftModuleCmd :: ModuleCmd a -> REPL a moduleCmdResult :: ModuleRes a -> REPL a instance GHC.Show.Show Cryptol.REPL.Command.QCMode instance GHC.Classes.Eq Cryptol.REPL.Command.QCMode instance GHC.Show.Show Cryptol.REPL.Command.CommandDescr instance GHC.Classes.Eq Cryptol.REPL.Command.CommandDescr instance GHC.Classes.Ord Cryptol.REPL.Command.CommandDescr