-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Cryptol: The Language of Cryptography -- @package cryptol @version 2.2.2 module Cryptol.Version commitHash :: String commitShortHash :: String commitBranch :: String commitDirty :: Bool -- | 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.Panic panic :: String -> [String] -> a instance [safe] Typeable CryptolPanic instance [safe] Exception CryptolPanic instance [safe] Show CryptolPanic -- | 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 algerbaic 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 algeibraic 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' -- | 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' nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat' 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 instance [safe] Show Nat' instance [safe] Eq Nat' instance [safe] Ord Nat' -- | This module defines intervals and interval arithmetic. module Cryptol.TypeCheck.Solver.Interval -- | Representation of intervals. Intervals always include the lower bound. -- Intervals include the upper bound if: * either the upper bound is -- finite, or * the upper bound is Inf and isFinite == -- False. -- -- Invariant: if the upper bound is finite, then `isFinite == True`. -- -- 
--   [x,y]     Interval (Nat x) (Nat y) True
--   [x,inf]   Interval (Nat x) Inf     False
--   [x,inf)   Interval (Nat x) Inf     True
--
data Interval Interval :: Nat' -> Nat' -> Bool -> Interval -- | Lower bound lowerBound :: Interval -> Nat' -- | Upper bound upperBound :: Interval -> Nat' -- | Do we know this to be a finite value. Note that for [inf,inf] -- this field is False (i.e., this field is not talking about the -- size of the interval, but, rather, about if it contains infinity). isFinite :: Interval -> Bool -- | Any possible value. anything :: Interval iConst :: Nat' -> Interval iAdd :: Interval -> Interval -> Interval iMul :: Interval -> Interval -> Interval iExp :: Interval -> Interval -> Interval iMin :: Interval -> Interval -> Interval iMax :: Interval -> Interval -> Interval iLg2 :: Interval -> Interval iWidth :: Interval -> Interval iSub :: Interval -> Interval -> Interval iDiv :: Interval -> Interval -> Interval iMod :: Interval -> Interval -> Interval iLenFromThen :: Interval -> Interval -> Interval -> Interval iLenFromTo :: Interval -> Interval -> Interval iLenFromThenTo :: Interval -> Interval -> Interval -> Interval -- | The first interval is definiately smaller iLeq :: Interval -> Interval -> Bool -- | The first interval is definiately smaller iLt :: Interval -> Interval -> Bool -- | The two intervals do not overlap. iDisjoint :: Interval -> Interval -> Bool instance [safe] Show Interval -- | 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.TypeCheck.Solver.CrySAT debug :: PropSet -> [S] data Prop Fin :: Expr -> Prop (:==) :: Expr -> Expr -> Prop (:/=) :: Expr -> Expr -> Prop (:>=) :: Expr -> Expr -> Prop (:>) :: Expr -> Expr -> Prop (:&&) :: Prop -> Prop -> Prop (:||) :: Prop -> Prop -> Prop Not :: Prop -> Prop data Expr K :: InfNat -> Expr Var :: Name -> Expr (:+) :: Expr -> Expr -> Expr (:-) :: Expr -> Expr -> Expr (:*) :: Expr -> Expr -> Expr Div :: Expr -> Expr -> Expr Mod :: Expr -> Expr -> Expr (:^^) :: Expr -> Expr -> Expr Min :: Expr -> Expr -> Expr Max :: Expr -> Expr -> Expr Lg2 :: Expr -> Expr Width :: Expr -> Expr LenFromThen :: Expr -> Expr -> Expr -> Expr LenFromThenTo :: Expr -> Expr -> Expr -> Expr data PropSet noProps :: PropSet assert :: Prop -> PropSet -> PropSet checkSat :: PropSet -> Result data Result Sat :: [(Int, InfNat)] -> Result Unsat :: Result Unknown :: Result data InfNat Nat :: Integer -> InfNat Inf :: InfNat data Name toName :: Int -> Name fromName :: Name -> Maybe Int instance [safe] Show Name instance [safe] Eq Name instance [safe] Ord Name instance [safe] Eq InfNat instance [safe] Ord InfNat instance [safe] Show InfNat instance [safe] Show Expr instance [safe] Show Prop instance [safe] Show Result instance [safe] Show NonLin instance [safe] MonadPlus FM instance [safe] Monad FM instance [safe] Alternative FM instance [safe] Applicative FM instance [safe] Functor FM module Cryptol.Symbolic.BitVector -- | Invariant: BV w x requires that 0 <= w and 0 <= x < 2^w. data BitVector BV :: Bool -> !Int -> !Integer -> BitVector signedcxt :: BitVector -> Bool width :: BitVector -> !Int val :: BitVector -> !Integer bitMask :: Int -> Integer -- | Smart constructor for bitvectors. bv :: Int -> Integer -> BitVector sbv :: Bool -> Int -> Integer -> BitVector unsigned :: Int -> Integer -> Integer signed :: Int -> Integer -> Integer same :: Int -> Int -> Int type SWord = SBV BitVector extract :: Int -> Int -> SWord -> SWord cat :: SWord -> SWord -> SWord literalSWord :: Int -> Integer -> SWord randomSBVBitVector :: Int -> IO (SBV BitVector) mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector) forallBV :: String -> Int -> Symbolic (SBV BitVector) forallBV_ :: Int -> Symbolic (SBV BitVector) existsBV :: String -> Int -> Symbolic (SBV BitVector) existsBV_ :: Int -> Symbolic (SBV BitVector) instance Eq BitVector instance Ord BitVector instance Show BitVector instance SDivisible (SBV BitVector) instance SDivisible BitVector instance FromBits (SBV BitVector) instance SIntegral BitVector instance SymWord BitVector instance HasKind BitVector instance FiniteBits (SBV BitVector) instance FiniteBits BitVector instance Bits BitVector instance Num BitVector instance SignCast SWord SWord 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 Show a => Show (Trie a) module Cryptol.Utils.PP class PP a ppPrec :: PP a => Int -> a -> Doc pp :: PP a => a -> Doc pretty :: PP a => a -> String optParens :: Bool -> 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 -- | 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 -- | 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 commaSep :: [Doc] -> Doc instance [safe] Show Assoc instance [safe] Eq Assoc 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 propegate. emptyRange :: Range start :: Position move :: Position -> Char -> Position moves :: Position -> String -> 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 instance [safe] Eq Position instance [safe] Ord Position instance [safe] Show Position instance [safe] Eq Range instance [safe] Show Range instance [safe] Eq a => Eq (Located a) instance [safe] Show a => Show (Located a) instance [safe] AddLoc (Located a) instance [safe] HasLoc a => HasLoc [a] instance [safe] (HasLoc a, HasLoc b) => HasLoc (a, b) instance [safe] HasLoc (Located a) instance [safe] HasLoc Range instance [safe] PP a => PP (Located a) instance [safe] PP Range instance [safe] PP Position instance [safe] Functor Located 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 -> String -> ([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 -> String -> ([Located Token], Position) data Layout Layout :: Layout NoLayout :: Layout data Token Token :: TokenT -> String -> Token tokenType :: Token -> TokenT tokenText :: Token -> String data TokenT -- | value, base, number of digits Num :: Integer -> Int -> Int -> TokenT -- | character literal ChrLit :: Char -> TokenT -- | identifier Ident :: String -> 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_Arith :: TokenKW KW_Bit :: TokenKW KW_Cmp :: TokenKW KW_False :: TokenKW KW_True :: TokenKW KW_else :: TokenKW KW_Eq :: TokenKW KW_error :: TokenKW KW_extern :: TokenKW KW_fin :: TokenKW KW_if :: TokenKW KW_private :: TokenKW KW_include :: TokenKW KW_inf :: TokenKW KW_join :: 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_pmult :: TokenKW KW_pdiv :: TokenKW KW_pmod :: TokenKW KW_property :: TokenKW KW_random :: TokenKW KW_reverse :: TokenKW KW_split :: TokenKW KW_splitAt :: TokenKW KW_then :: TokenKW KW_transpose :: TokenKW KW_type :: TokenKW KW_where :: TokenKW KW_let :: TokenKW KW_x :: TokenKW KW_zero :: TokenKW KW_import :: TokenKW KW_as :: TokenKW KW_hiding :: TokenKW data TokenErr UnterminatedComment :: TokenErr UnterminatedString :: TokenErr UnterminatedChar :: TokenErr InvalidString :: TokenErr InvalidChar :: TokenErr LexicalError :: TokenErr data TokenOp Plus :: TokenOp Minus :: TokenOp Mul :: TokenOp Div :: TokenOp Exp :: TokenOp Mod :: TokenOp NotEqual :: TokenOp Equal :: TokenOp LessThan :: TokenOp GreaterThan :: TokenOp LEQ :: TokenOp GEQ :: TokenOp EqualFun :: TokenOp NotEqualFun :: TokenOp ShiftL :: TokenOp ShiftR :: TokenOp RotL :: TokenOp RotR :: TokenOp Conj :: TokenOp Disj :: TokenOp Xor :: TokenOp Complement :: TokenOp Bang :: TokenOp BangBang :: TokenOp At :: TokenOp AtAt :: TokenOp Hash :: TokenOp 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 ColonColon :: 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 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 instance Functor AlexLastAcc 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 intToName :: Int -> String -- | Expand a list of base names into an infinite list of variations. nameList :: [String] -> [String] dump :: PP (WithNames a) => a -> String module Cryptol.Prims.Syntax -- | Built-in 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
--
TCLg2 :: TFun -- | 
--   : Num -> Num -> Num
--
TCExp :: TFun -- | 
--   : Num -> Num
--
TCWidth :: TFun -- | 
--   : Num -> Num -> Num
--
TCMin :: TFun -- | 
--   : Num -> Num -> Num
--
TCMax :: 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 -- | Built-in constants. data ECon ECTrue :: ECon ECFalse :: ECon -- | Converts a numeric type into its corresponding value. ECDemote :: ECon ECPlus :: ECon ECMinus :: ECon ECMul :: ECon ECDiv :: ECon ECMod :: ECon ECExp :: ECon ECLg2 :: ECon ECNeg :: ECon ECLt :: ECon ECGt :: ECon ECLtEq :: ECon ECGtEq :: ECon ECEq :: ECon ECNotEq :: ECon ECFunEq :: ECon ECFunNotEq :: ECon ECMin :: ECon ECMax :: ECon ECAnd :: ECon ECOr :: ECon ECXor :: ECon ECCompl :: ECon ECZero :: ECon ECShiftL :: ECon ECShiftR :: ECon ECRotL :: ECon ECRotR :: ECon ECCat :: ECon ECSplitAt :: ECon ECJoin :: ECon ECSplit :: ECon ECReverse :: ECon ECTranspose :: ECon ECAt :: ECon ECAtRange :: ECon ECAtBack :: ECon ECAtRangeBack :: ECon ECFromThen :: ECon ECFromTo :: ECon ECFromThenTo :: ECon ECInfFrom :: ECon ECInfFromThen :: ECon ECError :: ECon ECPMul :: ECon ECPDiv :: ECon ECPMod :: ECon ECRandom :: ECon eBinOpPrec :: Map ECon (Assoc, Int) tBinOpPrec :: Map TFun (Assoc, Int) ppPrefix :: ECon -> Doc instance Show TFun instance Eq TFun instance Ord TFun instance Bounded TFun instance Enum TFun instance Eq ECon instance Ord ECon instance Show ECon instance Bounded ECon instance Enum ECon instance PP ECon instance PP TFun module Cryptol.Parser.AST -- | Module names are just namespaces. -- -- INVARIANT: the list of strings should never be empty in a valid module -- name. newtype ModName ModName :: [String] -> ModName modRange :: Module -> Range data QName QName :: (Maybe ModName) -> Name -> QName mkQual :: ModName -> Name -> QName mkUnqual :: Name -> QName unqual :: QName -> Name data Name Name :: String -> Name NewName :: Pass -> Int -> Name data Named a Named :: Located Name -> a -> Named a name :: Named a -> Located Name value :: Named a -> a data Pass NoPat :: Pass MonoValues :: Pass data Schema Forall :: [TParam] -> [Prop] -> Type -> (Maybe Range) -> Schema data TParam TParam :: Name -> Maybe Kind -> Maybe Range -> TParam tpName :: TParam -> Name tpKind :: TParam -> Maybe Kind tpRange :: TParam -> Maybe Range tpQName :: TParam -> QName data Kind KNum :: Kind KType :: Kind data Type -- | 
--   [8] -> [8]
--
TFun :: Type -> Type -> Type -- | 
--   [8] a
--
TSeq :: Type -> Type -> Type -- | 
--   Bit
--
TBit :: Type -- | 
--   10
--
TNum :: Integer -> Type -- | 
--   a
--
TChar :: Char -> Type -- | 
--   inf
--
TInf :: Type -- | A type variable or synonym TUser :: QName -> [Type] -> Type -- | 
--   2 + x
--
TApp :: TFun -> [Type] -> Type -- | 
--   { x : [8], y : [32] }
--
TRecord :: [Named Type] -> Type -- | 
--   ([8], [32])
--
TTuple :: [Type] -> Type -- | _, just some type. TWild :: Type -- | Location information TLocated :: Type -> Range -> Type data Prop -- | 
--   fin x
--
CFin :: Type -> Prop -- | 
--   x == 10
--
CEqual :: Type -> Type -> Prop -- | 
--   x >= 10
--
CGeq :: Type -> Type -> Prop -- | 
--   Arith a
--
CArith :: Type -> Prop -- | 
--   Cmp a
--
CCmp :: Type -> Prop -- | Location information CLocated :: Prop -> Range -> Prop data Module Module :: Located ModName -> [Located Import] -> [TopDecl] -> Module mName :: Module -> Located ModName mImports :: Module -> [Located Import] mDecls :: Module -> [TopDecl] newtype Program Program :: [TopDecl] -> Program data TopDecl Decl :: (TopLevel Decl) -> TopDecl TDNewtype :: (TopLevel Newtype) -> TopDecl Include :: (Located FilePath) -> TopDecl data Decl DSignature :: [LQName] -> Schema -> Decl DPragma :: [LQName] -> Pragma -> Decl DBind :: Bind -> Decl DPatBind :: Pattern -> Expr -> Decl DType :: TySyn -> Decl DLocated :: Decl -> Range -> Decl data TySyn TySyn :: LQName -> [TParam] -> Type -> TySyn -- | Bindings. Notes: -- -- data Bind Bind :: LQName -> [Pattern] -> Expr -> Maybe Schema -> [Pragma] -> Bool -> Bind -- | Defined thing bName :: Bind -> LQName -- | Parameters bParams :: Bind -> [Pattern] -- | Definition bDef :: Bind -> Expr -- | Optional type sig bSignature :: Bind -> Maybe Schema -- | Optional pragmas bPragmas :: Bind -> [Pragma] -- | Is this a monomorphic binding bMono :: Bind -> Bool data Pragma PragmaNote :: String -> Pragma PragmaProperty :: Pragma -- | Export information for a declaration. data ExportType Public :: ExportType Private :: ExportType data ExportSpec ExportSpec :: Set QName -> Set QName -> ExportSpec eTypes :: ExportSpec -> Set QName eBinds :: ExportSpec -> Set QName -- | Add a binding name to the export list, if it should be exported. exportBind :: TopLevel QName -> ExportSpec -- | Add a type synonym name to the export list, if it should be exported. exportType :: TopLevel QName -> ExportSpec -- | Check to see if a binding is exported. isExportedBind :: QName -> ExportSpec -> Bool -- | Check to see if a type synonym is exported. isExportedType :: QName -> ExportSpec -> Bool data TopLevel a TopLevel :: ExportType -> a -> TopLevel a tlExport :: TopLevel a -> ExportType 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 :: [Name] -> ImportSpec Only :: [Name] -> ImportSpec data Newtype Newtype :: LQName -> [TParam] -> [Named Type] -> Newtype -- | Type name nName :: Newtype -> LQName -- | Type params nParams :: Newtype -> [TParam] -- | Constructor nBody :: Newtype -> [Named Type] -- | Input at the REPL, which can either be an expression or a let -- statement. data ReplInput ExprInput :: Expr -> ReplInput LetInput :: Decl -> ReplInput data Expr -- | 
--   x
--
EVar :: QName -> Expr -- | 
--   split
--
ECon :: ECon -> Expr -- | 
--   0x10
--
ELit :: Literal -> Expr -- | 
--   (1,2,3)
--
ETuple :: [Expr] -> Expr -- | 
--   { x = 1, y = 2 }
--
ERecord :: [Named Expr] -> Expr -- | 
--   e.l
--
ESel :: Expr -> Selector -> Expr -- | 
--   [1,2,3]
--
EList :: [Expr] -> Expr -- | 
--   [1, 5 ..  117 ]
--
EFromTo :: Type -> (Maybe Type) -> (Maybe Type) -> Expr -- | 
--   [1, 3 ...]
--
EInfFrom :: Expr -> (Maybe Expr) -> Expr -- | 
--   [ 1 | x <- xs ]
--
EComp :: Expr -> [[Match]] -> Expr -- | 
--   f x
--
EApp :: Expr -> Expr -> Expr -- | 
--   f `{x = 8}, f`{8}
--
EAppT :: Expr -> [TypeInst] -> Expr -- | 
--   if ok then e1 else e2
--
EIf :: Expr -> Expr -> Expr -> Expr -- | 
--   1 + x where { x = 2 }
--
EWhere :: Expr -> [Decl] -> Expr -- | 
--   1 : [8]
--
ETyped :: Expr -> Type -> Expr -- | `(x + 1), x is a type ETypeVal :: Type -> Expr -- | 
--   \x y -> x
--
EFun :: [Pattern] -> Expr -> Expr -- | position annotation ELocated :: Expr -> Range -> Expr -- | 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 -- | p <- e Match :: Pattern -> Expr -> Match MatchLet :: Bind -> Match data Pattern -- | 
--   x
--
PVar :: LName -> Pattern -- | 
--   _
--
PWild :: Pattern -- | 
--   (x,y,z)
--
PTuple :: [Pattern] -> Pattern -- | 
--   { x = (a,b,c), y = z }
--
PRecord :: [Named Pattern] -> Pattern -- | 
--   [ x, y, z ]
--
PList :: [Pattern] -> Pattern -- | 
--   x : [8]
--
PTyped :: Pattern -> Type -> Pattern -- | 
--   (x # y)
--
PSplit :: Pattern -> Pattern -> Pattern -- | Location information PLocated :: Pattern -> Range -> Pattern -- | 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 :: Name -> (Maybe [Name]) -> Selector -- | List selection. Optionally specifies the length of the list. ListSel :: Int -> (Maybe Int) -> Selector data TypeInst NamedInst :: (Named Type) -> TypeInst PosInst :: Type -> TypeInst data Located a Located :: !Range -> a -> Located a srcRange :: Located a -> !Range thing :: Located a -> a -- | A name with location information. type LName = Located Name -- | A qualified name with location information. type LQName = Located QName -- | A string with location information. type LString = Located String 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 [safe] Eq ModName instance [safe] Ord ModName instance [safe] Show ModName instance [safe] Eq Pass instance [safe] Ord Pass instance [safe] Show Pass instance [safe] Eq Name instance [safe] Ord Name instance [safe] Show Name instance [safe] Eq QName instance [safe] Ord QName instance [safe] Show QName instance [safe] Eq ImportSpec instance [safe] Show ImportSpec instance [safe] Eq Import instance [safe] Show Import instance [safe] Eq Pragma instance [safe] Show Pragma instance [safe] Eq ExportType instance [safe] Show ExportType instance [safe] Ord ExportType instance [safe] Show a => Show (TopLevel a) instance [safe] Eq a => Eq (TopLevel a) instance [safe] Ord a => Ord (TopLevel a) instance [safe] Show ExportSpec instance [safe] Eq NumInfo instance [safe] Show NumInfo instance [safe] Eq Literal instance [safe] Show Literal instance [safe] Eq Selector instance [safe] Show Selector instance [safe] Ord Selector instance [safe] Eq a => Eq (Named a) instance [safe] Show a => Show (Named a) instance [safe] Eq Kind instance [safe] Show Kind instance [safe] Eq TParam instance [safe] Show TParam instance [safe] Eq Type instance [safe] Show Type instance [safe] Eq Pattern instance [safe] Show Pattern instance [safe] Eq TypeInst instance [safe] Show TypeInst instance [safe] Eq Newtype instance [safe] Show Newtype instance [safe] Eq TySyn instance [safe] Show TySyn instance [safe] Eq Prop instance [safe] Show Prop instance [safe] Eq Schema instance [safe] Show Schema instance [safe] Eq Decl instance [safe] Show Decl instance [safe] Eq Expr instance [safe] Show Expr instance [safe] Eq Match instance [safe] Show Match instance [safe] Eq Bind instance [safe] Show Bind instance [safe] Eq ReplInput instance [safe] Show ReplInput instance [safe] Eq TopDecl instance [safe] Show TopDecl instance [safe] Eq Module instance [safe] Show Module instance [safe] Eq Program instance [safe] Show Program instance [safe] NoPos Prop instance [safe] NoPos Type instance [safe] NoPos TParam instance [safe] NoPos Schema instance [safe] NoPos Pattern instance [safe] NoPos Match instance [safe] NoPos TypeInst instance [safe] NoPos Expr instance [safe] NoPos TySyn instance [safe] NoPos Pragma instance [safe] NoPos Bind instance [safe] NoPos Newtype instance [safe] NoPos Decl instance [safe] NoPos a => NoPos (TopLevel a) instance [safe] NoPos TopDecl instance [safe] NoPos Module instance [safe] NoPos Program instance [safe] NoPos t => NoPos (Maybe t) instance [safe] NoPos t => NoPos [t] instance [safe] NoPos t => NoPos (Named t) instance [safe] NoPos (Located t) instance [safe] PP Prop instance [safe] PP Type instance [safe] PP TParam instance [safe] PP Kind instance [safe] PP Schema instance [safe] PP Match instance [safe] PP Pattern instance [safe] PP Selector instance [safe] PP Expr instance [safe] PP TypeInst instance [safe] PP Literal instance [safe] PP Name instance [safe] PP QName instance [safe] PP ModName instance [safe] PP TySyn instance [safe] PP Bind instance [safe] PP Pragma instance [safe] PP a => PP (TopLevel a) instance [safe] PP ImportSpec instance [safe] PP Import instance [safe] PP Newtype instance [safe] PP Decl instance [safe] PP TopDecl instance [safe] PP Program instance [safe] PP Module instance [safe] HasLoc Newtype instance [safe] HasLoc Module instance [safe] HasLoc TopDecl instance [safe] HasLoc a => HasLoc (TopLevel a) instance [safe] AddLoc Decl instance [safe] HasLoc Decl instance [safe] AddLoc Schema instance [safe] HasLoc Schema instance [safe] HasLoc a => HasLoc (Named a) instance [safe] HasLoc Match instance [safe] HasLoc Bind instance [safe] HasLoc Pattern instance [safe] AddLoc Pattern instance [safe] AddLoc Prop instance [safe] HasLoc Prop instance [safe] AddLoc Type instance [safe] HasLoc Type instance [safe] AddLoc TParam instance [safe] HasLoc TParam instance [safe] HasLoc Expr instance [safe] AddLoc Expr instance [safe] Functor Named instance [safe] Monoid ExportSpec instance [safe] Functor TopLevel module Cryptol.TypeCheck.AST -- | A Cryptol module. data Module Module :: ModName -> ExportSpec -> [Import] -> Map QName TySyn -> Map QName Newtype -> [DeclGroup] -> Module mName :: Module -> ModName mExports :: Module -> ExportSpec mImports :: Module -> [Import] mTySyns :: Module -> Map QName TySyn mNewtypes :: Module -> Map QName Newtype mDecls :: Module -> [DeclGroup] -- | Kinds, classify types. data Kind KType :: Kind KNum :: Kind KProp :: Kind (:->) :: Kind -> Kind -> Kind -- | The types of polymorphic values. data Schema Forall :: [TParam] -> [Prop] -> Type -> Schema sVars :: Schema -> [TParam] sProps :: Schema -> [Prop] sType :: Schema -> Type -- | Type synonym. data TySyn TySyn :: QName -> [TParam] -> [Prop] -> Type -> TySyn -- | Name tsName :: TySyn -> QName -- | Parameters tsParams :: TySyn -> [TParam] -- | Ensure body is OK tsConstraints :: TySyn -> [Prop] -- | Definition tsDef :: TySyn -> Type -- | Named records data Newtype Newtype :: QName -> [TParam] -> [Prop] -> [(Name, Type)] -> Newtype ntName :: Newtype -> QName ntParams :: Newtype -> [TParam] ntConstraints :: Newtype -> [Prop] ntFields :: Newtype -> [(Name, Type)] -- | Type parameters. data TParam TParam :: !Int -> Kind -> Maybe QName -> TParam -- | Parameter identifier tpUnique :: TParam -> !Int -- | Kind of parameter tpKind :: TParam -> Kind -- | Name from source, if any. tpName :: TParam -> Maybe QName tpVar :: 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 :: QName -> [Type] -> Type -> Type -- | Record type TRec :: [(Name, Type)] -> Type -- | The type is supposed to be of kind KProp type Prop = Type -- | The type is "simple" (i.e., it contains no type functions). type SType = Type -- | Type variables. data TVar -- | Unique, kind, ids of bound type variables that are in scope The -- Doc is a description of how this type came to be. TVFree :: !Int -> Kind -> (Set TVar) -> Doc -> TVar TVBound :: !Int -> Kind -> TVar -- | Type constants. data TCon TC :: TC -> TCon PC :: PC -> TCon TF :: TFun -> TCon -- | Built-in type constants. -- -- Predicate symbols. data PC -- | 
--   _ == _
--
PEqual :: PC -- | 
--   _ /= _
--
PNeq :: PC -- | 
--   _ >= _
--
PGeq :: PC -- | 
--   fin _
--
PFin :: PC -- | Has sel type field does not appear in schemas PHas :: Selector -> PC -- | 
--   Arith _
--
PArith :: PC -- | 
--   Cmp _
--
PCmp :: PC -- | 1-1 constants. data TC -- | Numbers TCNum :: Integer -> TC -- | Inf TCInf :: TC -- | Bit TCBit :: TC -- | 
--   [_] _
--
TCSeq :: TC -- | 
--   _ -> _
--
TCFun :: TC -- | 
--   (_, _, _)
--
TCTuple :: Int -> TC -- | user-defined, T TCNewtype :: UserTC -> TC data UserTC UserTC :: QName -> Kind -> UserTC data Expr -- | Built-in constant ECon :: ECon -> Expr -- | List value (with type of elements) EList :: [Expr] -> Type -> Expr -- | Tuple value ETuple :: [Expr] -> Expr -- | Record value ERec :: [(Name, Expr)] -> Expr -- | Elimination for tuplerecordlist ESel :: Expr -> Selector -> Expr -- | If-then-else EIf :: Expr -> Expr -> Expr -> Expr -- | List comprehensions The type caches the type of the expr. EComp :: Type -> Expr -> [[Match]] -> Expr -- | Use of a bound variable EVar :: QName -> Expr -- | Function Value ETAbs :: TParam -> Expr -> Expr -- | Type application ETApp :: Expr -> Type -> Expr -- | Function application EApp :: Expr -> Expr -> Expr -- | Function value EAbs :: QName -> 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 -- | if e : t1, then cast e : t2 as long as we can prove that 't1 = t2'. We -- could express this in terms of a built-in constant. `cast :: {a,b} (a -- =*= b) => a -> b` -- -- Using the constant is a bit verbose though, because we end up with -- both the source and target type. So, instead we use this language -- construct, which only stores the target type, and the source type can -- be reconstructed from the expression. -- -- Another way to think of this is simply as an expression with an -- explicit type annotation. ECast :: Expr -> Type -> Expr EWhere :: Expr -> [DeclGroup] -> Expr data Match -- | do we need this type? it seems like it can be computed from the expr From :: QName -> Type -> Expr -> Match Let :: Decl -> Match data DeclGroup -- | Mutually recursive declarations Recursive :: [Decl] -> DeclGroup -- | Non-recursive declaration NonRecursive :: Decl -> DeclGroup groupDecls :: DeclGroup -> [Decl] data Decl Decl :: QName -> Schema -> Expr -> [Pragma] -> Decl dName :: Decl -> QName dSignature :: Decl -> Schema dDefinition :: Decl -> Expr dPragmas :: Decl -> [Pragma] isFreeTV :: TVar -> Bool isBoundTV :: TVar -> Bool tIsNum :: Type -> Maybe Integer tIsInf :: Type -> Bool tIsVar :: Type -> Maybe TVar tIsFun :: Type -> Maybe (Type, Type) tIsSeq :: Type -> Maybe (Type, Type) tIsBit :: Type -> Bool tIsTuple :: Type -> Maybe [Type] pIsFin :: Prop -> Maybe Type pIsGeq :: Prop -> Maybe (Type, Type) pIsEq :: Prop -> Maybe (Type, Type) pIsArith :: Prop -> Maybe Type pIsCmp :: Prop -> Maybe Type pIsNumeric :: Prop -> Bool tNum :: Integral a => a -> Type tZero :: Type tOne :: Type tTwo :: Type tInf :: Type tBit :: Type eTrue :: Expr eFalse :: Expr tWord :: Type -> Type tSeq :: Type -> Type -> Type tChar :: Type eChar :: Char -> Expr tString :: Int -> Type eString :: String -> Expr -- | Make an expression that is error pre-applied to a type and a -- message. eError :: Type -> String -> Expr tRec :: [(Name, Type)] -> Type tTuple :: [Type] -> Type -- | Make a function type. tFun :: Type -> Type -> Type -- | Eliminate type synonyms. tNoUser :: Type -> Type tWidth :: Type -> Type tLenFromThen :: Type -> Type -> Type -> Type tLenFromThenTo :: Type -> Type -> Type -> Type tMax :: Type -> Type -> Type -- | Equality for numeric types. (=#=) :: Type -> Type -> Prop (=/=) :: Type -> Type -> Prop pArith :: Type -> Prop pCmp :: Type -> Prop -- | Make a greater-than-or-equal-to constraint. (>==) :: Type -> Type -> Prop -- | A Has constraint, used for tuple and record selection. pHas :: Selector -> Type -> Type -> Prop pFin :: Type -> Prop -- | Make multiplication type. (.*.) :: Type -> Type -> Type -- | Make addition type. (.+.) :: Type -> Type -> Type (.-.) :: Type -> Type -> Type (.^.) :: Type -> Type -> Type tDiv :: Type -> Type -> Type tMod :: Type -> Type -> Type -- | Make a min type. tMin :: Type -> Type -> Type newtypeTyCon :: Newtype -> TCon newtypeConType :: Newtype -> Schema class HasKind t kindOf :: HasKind t => t -> Kind quickApply :: Kind -> [a] -> Kind addTNames :: [TParam] -> NameMap -> NameMap ppNewtypeShort :: Newtype -> Doc ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(QName, Type)] -> Expr -> Doc splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) splitAbs :: Expr -> Maybe ((QName, Type), Expr) splitTAbs :: Expr -> Maybe (TParam, Expr) splitProofAbs :: Expr -> Maybe (Prop, Expr) -- | Built-in 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
--
TCLg2 :: TFun -- | 
--   : Num -> Num -> Num
--
TCExp :: TFun -- | 
--   : Num -> Num
--
TCWidth :: TFun -- | 
--   : Num -> Num -> Num
--
TCMin :: TFun -- | 
--   : Num -> Num -> Num
--
TCMax :: 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 data Name Name :: String -> Name NewName :: Pass -> Int -> Name data QName QName :: (Maybe ModName) -> Name -> QName mkUnqual :: Name -> QName unqual :: QName -> Name -- | Module names are just namespaces. -- -- INVARIANT: the list of strings should never be empty in a valid module -- name. newtype ModName ModName :: [String] -> ModName -- | 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 :: Name -> (Maybe [Name]) -> 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 :: [Name] -> ImportSpec Only :: [Name] -> ImportSpec -- | Export information for a declaration. data ExportType Public :: ExportType Private :: ExportType data ExportSpec ExportSpec :: Set QName -> Set QName -> ExportSpec eTypes :: ExportSpec -> Set QName eBinds :: ExportSpec -> Set QName -- | Check to see if a binding is exported. isExportedBind :: QName -> ExportSpec -> Bool -- | Check to see if a type synonym is exported. isExportedType :: QName -> ExportSpec -> Bool data Pragma PragmaNote :: String -> Pragma PragmaProperty :: Pragma instance [safe] Eq Kind instance [safe] Show Kind instance [safe] Show TParam instance [safe] Show TVar instance [safe] Show PC instance [safe] Eq PC instance [safe] Ord PC instance [safe] Show UserTC instance [safe] Show TC instance [safe] Eq TC instance [safe] Ord TC instance [safe] Show TCon instance [safe] Eq TCon instance [safe] Ord TCon instance [safe] Show Type instance [safe] Eq Type instance [safe] Ord Type instance [safe] Show Newtype instance [safe] Eq TySyn instance [safe] Show TySyn instance [safe] Eq Schema instance [safe] Show Schema instance [safe] Show Decl instance [safe] Show Expr instance [safe] Show DeclGroup instance [safe] Show Match instance [safe] Show Module instance [safe] PP (WithNames Module) instance [safe] PP Module instance [safe] PP Decl instance [safe] PP (WithNames Decl) instance [safe] PP DeclGroup instance [safe] PP (WithNames DeclGroup) instance [safe] PP Match instance [safe] PP (WithNames Match) instance [safe] PP Expr instance [safe] PP (WithNames Expr) instance [safe] PP UserTC instance [safe] PP TC instance [safe] PP PC instance [safe] PP TCon instance [safe] PP Type instance [safe] PP (WithNames TySyn) instance [safe] PP TySyn instance [safe] PP (WithNames Schema) instance [safe] PP Schema instance [safe] PP (WithNames Type) instance [safe] PP (WithNames TParam) instance [safe] PP TParam instance [safe] PP (WithNames TVar) instance [safe] PP Kind instance [safe] HasKind TParam instance [safe] HasKind Newtype instance [safe] HasKind TySyn instance [safe] HasKind Type instance [safe] HasKind TFun instance [safe] HasKind PC instance [safe] HasKind TC instance [safe] HasKind UserTC instance [safe] HasKind TCon instance [safe] HasKind TVar instance [safe] Ord TVar instance [safe] Eq TVar instance [safe] Ord UserTC instance [safe] Eq UserTC instance [safe] Ord TParam instance [safe] Eq TParam module Cryptol.Prims.Types -- | Types of built-in constants. typeOf :: ECon -> Schema module Cryptol.Prims.Doc helpDoc :: ECon -> Doc description :: ECon -> Doc module Cryptol.Eval.Error -- | Panic from an Eval context. evalPanic :: String -> [String] -> a data EvalError InvalidIndex :: Integer -> EvalError TypeCannotBeDemoted :: Type -> EvalError DivideByZero :: EvalError WordTooWide :: Integer -> EvalError UserError :: String -> EvalError -- | A sequencing operation has gotten an invalid index. invalidIndex :: Integer -> a -- | For things like `(inf) or `(0-1) typeCannotBeDemoted :: Type -> a -- | For division by 0. divideByZero :: 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 error cryUserError :: String -> a instance [safe] Typeable EvalError instance [safe] Show EvalError instance [safe] Exception EvalError instance [safe] PP EvalError module Cryptol.Eval.Value isTBit :: TValue -> Bool isTSeq :: TValue -> Maybe (TValue, TValue) isTFun :: TValue -> Maybe (TValue, TValue) isTTuple :: TValue -> Maybe (Int, [TValue]) isTRec :: TValue -> Maybe [(Name, TValue)] tvSeq :: TValue -> TValue -> TValue numTValue :: TValue -> Nat' toNumTValue :: Nat' -> TValue finTValue :: TValue -> Integer data BV -- | width, value The value may contain junk bits BV :: !Integer -> !Integer -> BV -- | Smart constructor for BVs that checks for the width limit mkBv :: Integer -> Integer -> BV -- | Generic value type, parameterized by bit and word types. data GenValue b w VRecord :: [(Name, GenValue b w)] -> GenValue b w VTuple :: [GenValue b w] -> GenValue b w VBit :: b -> GenValue b w VSeq :: Bool -> [GenValue b w] -> GenValue b w VWord :: w -> GenValue b w VStream :: [GenValue b w] -> GenValue b w VFun :: (GenValue b w -> GenValue b w) -> GenValue b w VPoly :: (TValue -> GenValue b w) -> GenValue b w type Value = GenValue Bool BV -- | An evaluated type. These types do not contain type variables, type -- synonyms, or type functions. newtype TValue TValue :: Type -> TValue tValTy :: TValue -> Type data PPOpts PPOpts :: Bool -> Int -> Int -> PPOpts useAscii :: PPOpts -> Bool useBase :: PPOpts -> Int useInfLength :: PPOpts -> Int defaultPPOpts :: PPOpts ppValue :: PPOpts -> Value -> Doc asciiMode :: PPOpts -> Integer -> Bool integerToChar :: Integer -> Char data WithBase a WithBase :: PPOpts -> a -> WithBase a ppWord :: PPOpts -> BV -> Doc class BitWord b w packWord :: BitWord b w => [b] -> w unpackWord :: BitWord b w => w -> [b] mask :: Integer -> Integer -> Integer -- | Create a packed word of n bits. word :: Integer -> Integer -> Value lam :: (GenValue b w -> GenValue b w) -> GenValue b w -- | A type lambda that expects a Type. tlam :: (TValue -> GenValue b w) -> GenValue b w -- | Generate a stream. toStream :: [GenValue b w] -> GenValue b w toFinSeq :: TValue -> [GenValue b w] -> GenValue b w -- | 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 :: TValue -> TValue -> [GenValue b w] -> GenValue b w -- | Construct one of: * a word, when the sequence is finite and the -- elements are bits * a sequence, when the sequence is finite but the -- elements aren't bits * a stream, when the sequence is not finite -- -- NOTE: do not use this constructor in the case where the thing may be a -- finite, but recursive, sequence. toPackedSeq :: TValue -> TValue -> [Value] -> Value -- | Extract a bit value. fromVBit :: GenValue b w -> b -- | Extract a sequence. fromSeq :: BitWord b w => GenValue b w -> [GenValue b w] fromStr :: Value -> String -- | Extract a packed word. Note that this does not clean-up any junk bits -- in the word. fromVWord :: BitWord b w => GenValue b w -> w vWordLen :: Value -> Maybe Integer -- | Turn a value into an integer represented by w bits. fromWord :: Value -> Integer -- | Extract a function from a value. fromVFun :: GenValue b w -> (GenValue b w -> GenValue b w) -- | Extract a polymorphic function from a value. fromVPoly :: GenValue b w -> (TValue -> GenValue b w) -- | Extract a tuple from a value. fromVTuple :: GenValue b w -> [GenValue b w] -- | Extract a record from a value. fromVRecord :: GenValue b w -> [(Name, GenValue b w)] -- | Lookup a field in a record. lookupRecord :: Name -> GenValue b w -> GenValue b w -- | 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 :: Type -> Value -> Maybe Expr instance [safe] Functor WithBase instance [safe] BitWord Bool BV instance [safe] PP (WithBase Value) instance [safe] Show TValue -- | Evaluate test cases and handle exceptions appropriately module Cryptol.Testing.Eval -- | 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 -- | 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 :: Value -> [Value] -> IO TestResult module Cryptol.Symbolic.Value type Value = GenValue SBool SWord -- | An evaluated type. These types do not contain type variables, type -- synonyms, or type functions. data TValue numTValue :: TValue -> Nat' toNumTValue :: Nat' -> TValue finTValue :: TValue -> Integer isTBit :: TValue -> Bool isTFun :: TValue -> Maybe (TValue, TValue) isTSeq :: TValue -> Maybe (TValue, TValue) isTTuple :: TValue -> Maybe (Int, [TValue]) isTRec :: TValue -> Maybe [(Name, TValue)] tvSeq :: TValue -> TValue -> TValue -- | Generic value type, parameterized by bit and word types. data GenValue b w VRecord :: [(Name, GenValue b w)] -> GenValue b w VTuple :: [GenValue b w] -> GenValue b w VBit :: b -> GenValue b w VSeq :: Bool -> [GenValue b w] -> GenValue b w VWord :: w -> GenValue b w VStream :: [GenValue b w] -> GenValue b w VFun :: (GenValue b w -> GenValue b w) -> GenValue b w VPoly :: (TValue -> GenValue b w) -> GenValue b w lam :: (GenValue b w -> GenValue b w) -> GenValue b w -- | A type lambda that expects a Type. tlam :: (TValue -> GenValue b w) -> GenValue b w -- | Generate a stream. toStream :: [GenValue b w] -> GenValue b w toFinSeq :: TValue -> [GenValue b w] -> GenValue b w -- | 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 :: TValue -> TValue -> [GenValue b w] -> GenValue b w -- | Extract a bit value. fromVBit :: GenValue b w -> b -- | Extract a function from a value. fromVFun :: GenValue b w -> (GenValue b w -> GenValue b w) -- | Extract a polymorphic function from a value. fromVPoly :: GenValue b w -> (TValue -> GenValue b w) -- | Extract a tuple from a value. fromVTuple :: GenValue b w -> [GenValue b w] -- | Extract a record from a value. fromVRecord :: GenValue b w -> [(Name, GenValue b w)] -- | Lookup a field in a record. lookupRecord :: Name -> GenValue b w -> GenValue b w -- | Extract a sequence. fromSeq :: BitWord b w => GenValue b w -> [GenValue b w] -- | Extract a packed word. Note that this does not clean-up any junk bits -- in the word. fromVWord :: BitWord b w => GenValue b w -> w evalPanic :: String -> [String] -> a instance BitWord SBool SWord instance Mergeable Value -- | This module generates random values for Cryptol types. module Cryptol.Testing.Random type Gen g = Int -> g -> (Value, 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 => Value -> [Gen g] -> Int -> 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] -- | A generator for values of the given type. This fails if we are given a -- type that lacks a suitable random value generator. randomValue :: RandomGen g => Type -> Maybe (Gen g) -- | Generate a random bit value. randomBit :: RandomGen g => Gen g -- | 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 :: RandomGen g => Integer -> Gen g -- | Generate a random infinite stream value. randomStream :: RandomGen g => Gen g -> Gen g -- | Generate a random sequence. Generally, this should be used for -- sequences other than bits. For sequences of bits use "randomWord". The -- difference is mostly about how the results will be displayed. randomSequence :: RandomGen g => Integer -> Gen g -> Gen g -- | Generate a random tuple value. randomTuple :: RandomGen g => [Gen g] -> Gen g -- | Generate a random record value. randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g module Cryptol.Eval.Env type ReadEnv = EvalEnv data EvalEnv EvalEnv :: Map QName Value -> Map TVar TValue -> EvalEnv envVars :: EvalEnv -> Map QName Value envTypes :: EvalEnv -> Map TVar TValue emptyEnv :: EvalEnv -- | Bind a variable in the evaluation environment. bindVar :: QName -> Value -> EvalEnv -> EvalEnv -- | Lookup a variable in the environment. lookupVar :: QName -> EvalEnv -> Maybe Value -- | Bind a type variable of kind *. bindType :: TVar -> TValue -> EvalEnv -> EvalEnv -- | Lookup a type variable. lookupType :: TVar -> EvalEnv -> Maybe TValue instance [safe] PP (WithBase EvalEnv) instance [safe] Monoid EvalEnv module Cryptol.Eval.Type -- | Evaluation for types. evalType :: EvalEnv -> Type -> TValue -- | Reduce type functions, rising an exception for undefined values. evalTF :: TFun -> [TValue] -> TValue module Cryptol.Prims.Eval evalECon :: ECon -> Value -- | Make a numeric constant. ecDemoteV :: Value divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer) -- | Create a packed word modExp :: Integer -> Integer -> Integer -> Integer doubleAndAdd :: Integer -> Integer -> Integer -> Integer type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w type Binary = GenBinary Bool BV binary :: GenBinary b w -> GenValue b w type GenUnary b w = TValue -> GenValue b w -> GenValue b w type Unary = GenUnary Bool BV unary :: GenUnary b w -> GenValue b w -- | Turn a normal binop on Integers into one that can also deal with a -- bitsize. liftBinArith :: (Integer -> Integer -> Integer) -> BinArith type BinArith = Integer -> Integer -> Integer -> Integer arithBinary :: BinArith -> Binary arithUnary :: (Integer -> Integer) -> Unary lg2 :: Integer -> Integer divWrap :: Integral a => a -> a -> a modWrap :: Integral a => a -> a -> a -- | Lexicographic ordering on two values. lexCompare :: TValue -> Value -> Value -> Ordering zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering -- | Process two elements based on their lexicographic ordering. cmpOrder :: (Ordering -> Bool) -> Binary withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary maxV :: Ordering -> TValue -> Value -> Value -> Value minV :: Ordering -> TValue -> Value -> Value -> Value funCmp :: (Ordering -> Bool) -> Value zeroV :: TValue -> Value -- | Join a sequence of sequences into a single sequence. joinV :: TValue -> TValue -> TValue -> Value -> Value splitAtV :: TValue -> TValue -> TValue -> Value -> Value -- | Split implementation. ecSplitV :: Value -- | Split into infinitely many chunks infChunksOf :: Integer -> [a] -> [[a]] -- | Split into finitely many chunks finChunksOf :: Integer -> Integer -> [a] -> [[a]] ccatV :: TValue -> TValue -> TValue -> Value -> Value -> Value -- | Merge two values given a binop. This is used for and, or and xor. logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary logicUnary :: (forall a. Bits a => a -> a) -> Unary logicShift :: (Integer -> Integer -> Int -> Integer) -> (TValue -> TValue -> [Value] -> Int -> [Value]) -> Value shiftLW :: Integer -> Integer -> Int -> Integer shiftLS :: TValue -> TValue -> [Value] -> Int -> [Value] shiftRW :: Integer -> Integer -> Int -> Integer shiftRS :: TValue -> TValue -> [Value] -> Int -> [Value] rotateLW :: Integer -> Integer -> Int -> Integer rotateLS :: TValue -> TValue -> [Value] -> Int -> [Value] rotateRW :: Integer -> Integer -> Int -> Integer rotateRS :: TValue -> TValue -> [Value] -> Int -> [Value] -- | Indexing operations that return one element. indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value indexFront :: Maybe Integer -> [Value] -> Integer -> Value indexBack :: Maybe Integer -> [Value] -> Integer -> Value -- | Indexing operations that return many elements. indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] fromThenV :: Value fromToV :: Value fromThenToV :: Value -- | 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 :: TValue -> Integer -> Value tlamN :: (Nat' -> GenValue b w) -> GenValue b w module Cryptol.Eval moduleEnv :: Module -> EvalEnv -> EvalEnv data EvalEnv emptyEnv :: EvalEnv evalExpr :: EvalEnv -> Expr -> Value evalDecls :: [DeclGroup] -> EvalEnv -> EvalEnv data EvalError InvalidIndex :: Integer -> EvalError TypeCannotBeDemoted :: Type -> EvalError DivideByZero :: EvalError WordTooWide :: Integer -> EvalError UserError :: String -> EvalError data WithBase a WithBase :: PPOpts -> a -> WithBase a module Cryptol.TypeCheck.TypeMap data TypeMap a TM :: Map TVar a -> Map TCon (List TypeMap a) -> Map [Name] (List TypeMap a) -> TypeMap a tvar :: TypeMap a -> Map TVar a tcon :: TypeMap a -> Map TCon (List TypeMap a) trec :: TypeMap a -> Map [Name] (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 [safe] Functor m => Functor (List m) instance [safe] Functor TypeMap instance [safe] Show a => Show (TypeMap a) instance [safe] TrieMap TypeMap Type instance [safe] Ord a => TrieMap (Map a) a instance [safe] TrieMap m a => TrieMap (List m) [a] module Cryptol.TypeCheck.Subst data Subst S :: Map TVar Type -> !Bool -> Subst suMap :: Subst -> Map TVar Type suDefaulting :: Subst -> !Bool 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 substToList :: Subst -> Maybe [(TVar, Type)] class FVS t fvs :: FVS t => t -> Set TVar class TVars t apSubst :: TVars t => Subst -> t -> t -- | Pick types for unconstrained unification variables. defaultFreeVar :: TVar -> Type -- | Apply the substitution to the keys of a type map. apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a -- | WARNING: This instance assumes that the quantified variables in the -- types in the substitution will not get captured by the quantified -- variables. This is reasonable because there should be no shadowing of -- quantified variables but, just in case, we make a sanity check and -- panic if somehow capture did occur. instance [safe] Show Subst instance [safe] TVars Module instance [safe] TVars Decl instance [safe] TVars DeclGroup instance [safe] TVars Match instance [safe] TVars Expr instance [safe] TVars Schema instance [safe] TVars a => TVars (TypeMap a) instance [safe] (Functor m, TVars a) => TVars (List m a) instance [safe] TVars Type instance [safe] (TVars s, TVars t) => TVars (s, t) instance [safe] TVars t => TVars [t] instance [safe] TVars t => TVars (Maybe t) instance [safe] FVS Schema instance [safe] (FVS a, FVS b) => FVS (a, b) instance [safe] FVS a => FVS [a] instance [safe] FVS Type instance [safe] PP Subst instance [safe] PP (WithNames Subst) module Cryptol.TypeCheck.Unify -- | The most general unifier is a substitution and a set of constraints on -- bound variables. type MGU = (Subst, [Prop]) data Result a OK :: a -> Result a Error :: UnificationError -> Result a data UnificationError UniTypeMismatch :: Type -> Type -> UnificationError UniKindMismatch :: Kind -> Kind -> UnificationError UniTypeLenMismatch :: Int -> Int -> UnificationError UniRecursive :: TVar -> Type -> UnificationError UniNonPolyDepends :: TVar -> [TVar] -> UnificationError UniNonPoly :: TVar -> Type -> UnificationError uniError :: UnificationError -> Result a emptyMGU :: MGU mgu :: Type -> Type -> Result MGU mguMany :: [Type] -> [Type] -> Result MGU bindVar :: TVar -> Type -> Result MGU instance [safe] Functor Result instance [safe] Monad Result instance [safe] Applicative Result 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 QName Schema -> Expr -> Type fastSchemaOf :: Map QName Schema -> Expr -> Schema module Cryptol.TypeCheck.Solver.Utils splitMins :: Type -> [Type] -- | 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) module Cryptol.Testing.Exhaust -- | Given a (function) type, compute all possible inputs for it. We also -- return the total number of test (i.e., the length of the outer list. testableType :: Type -> Maybe (Integer, [[Value]]) -- | Apply a testable value to some arguments. Please note that this -- function assumes that the values come from a call to -- testableType (i.e., things are type-correct) runOneTest :: Value -> [Value] -> IO TestResult -- | Given a fully-evaluated type, try to compute the number of values in -- it. Returns Nothing for infinite types, user-defined types, -- polymorhic 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] -- | This module defines the scoping rules for value- and type-level names -- in Cryptol. module Cryptol.Parser.Names modExports :: Module -> ExportSpec -- | The names defined by a newtype. tnamesNT :: Newtype -> ([Located QName], ()) -- | The names defined and used by a group of mutually recursive -- declarations. namesDs :: [Decl] -> ([Located QName], Set QName) -- | The names defined and used by a single declarations. namesD :: Decl -> ([Located QName], Set QName) -- | 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 :: Decl -> [Located QName] tsName :: TySyn -> Located QName -- | The names defined and used by a single binding. namesB :: Bind -> ([Located QName], Set QName) -- | The names used by an expression. namesE :: Expr -> Set QName -- | The names defined by a group of patterns. namesPs :: [Pattern] -> [Located QName] -- | The names defined by a pattern. These will always be unqualified -- names. namesP :: Pattern -> [Located QName] -- | The names defined and used by a match. namesM :: Match -> ([Located QName], Set QName) -- | The names defined and used by an arm of alist comprehension. namesArm :: [Match] -> ([Located QName], Set QName) -- | Remove some defined variables from a set of free variables. boundNames :: [Located QName] -> Set QName -> Set QName -- | Given the set of type variables that are in scope, compute the type -- synonyms used by a type. namesT :: Set QName -> Type -> Set QName -- | The type names defined and used by a group of mutually recursive -- declarations. tnamesDs :: [Decl] -> ([Located QName], Set QName) -- | The type names defined and used by a single declaration. tnamesD :: Decl -> ([Located QName], Set QName) -- | The type names used by a single binding. tnamesB :: Bind -> Set QName -- | The type names used by an expression. tnamesE :: Expr -> Set QName tnamesTI :: TypeInst -> Set QName -- | The type names used by a pattern. tnamesP :: Pattern -> Set QName -- | The type names used by a match. tnamesM :: Match -> Set QName -- | The type names used by a type schema. tnamesS :: Schema -> Set QName -- | The type names used by a prop. tnamesC :: Prop -> Set QName -- | Compute the type synonyms/type variables used by a type. tnamesT :: Type -> Set QName module Cryptol.ModuleSystem.Interface -- | The resulting interface generated by a module that has been -- typechecked. data Iface Iface :: ModName -> IfaceDecls -> IfaceDecls -> Iface ifModName :: Iface -> ModName ifPublic :: Iface -> IfaceDecls ifPrivate :: Iface -> IfaceDecls data IfaceDecls IfaceDecls :: Map QName [IfaceTySyn] -> Map QName [IfaceNewtype] -> Map QName [IfaceDecl] -> IfaceDecls ifTySyns :: IfaceDecls -> Map QName [IfaceTySyn] ifNewtypes :: IfaceDecls -> Map QName [IfaceNewtype] ifDecls :: IfaceDecls -> Map QName [IfaceDecl] type IfaceTySyn = TySyn ifTySynName :: TySyn -> QName type IfaceNewtype = Newtype data IfaceDecl IfaceDecl :: QName -> Schema -> [Pragma] -> IfaceDecl ifDeclName :: IfaceDecl -> QName ifDeclSig :: IfaceDecl -> Schema ifDeclPragmas :: IfaceDecl -> [Pragma] mkIfaceDecl :: Decl -> IfaceDecl -- | Like mappend for IfaceDecls, but preferring entries on the left. shadowing :: IfaceDecls -> IfaceDecls -> IfaceDecls -- | Interpret an import declaration in the scope of the interface it -- targets. interpImport :: Import -> Iface -> Iface unqualified :: IfaceDecls -> IfaceDecls -- | Generate an Iface from a typechecked module. genIface :: Module -> Iface instance Show IfaceDecl instance Show IfaceDecls instance Show Iface instance Monoid IfaceDecls -- | 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 :: Module -> Module instance TrieMap RewMap' (QName, [Type], Int) module Cryptol.ModuleSystem.NamingEnv data NameOrigin Local :: (Located QName) -> NameOrigin Imported :: QName -> NameOrigin data EName EFromBind :: (Located QName) -> EName EFromNewtype :: (Located QName) -> EName EFromMod :: QName -> EName data TName TFromParam :: QName -> TName TFromSyn :: (Located QName) -> TName TFromNewtype :: (Located QName) -> TName TFromMod :: QName -> TName class HasQName a qname :: HasQName a => a -> QName origin :: HasQName a => a -> NameOrigin data NamingEnv NamingEnv :: Map QName [EName] -> Map QName [TName] -> NamingEnv -- | Expr renaming environment neExprs :: NamingEnv -> Map QName [EName] -- | Type renaming environment neTypes :: NamingEnv -> Map QName [TName] -- | Singleton type renaming environment. singletonT :: QName -> TName -> NamingEnv -- | Singleton expression renaming environment. singletonE :: QName -> EName -> NamingEnv -- | Like mappend, but when merging, prefer values on the lhs. shadowing :: NamingEnv -> NamingEnv -> NamingEnv travNamingEnv :: Applicative f => (QName -> f QName) -> NamingEnv -> f NamingEnv -- | Things that define exported names. class BindsNames a namingEnv :: BindsNames a => a -> NamingEnv -- | Generate a type renaming environment from the parameters that are -- bound by this schema. -- | Produce a naming environment from an interface file, that contains a -- mapping only from unqualified names to qualified ones. -- | Translate a set of declarations from an interface into a naming -- environment. -- | Translate names bound by the patterns of a match into a renaming -- environment. -- | Generate the naming environment for a type parameter. -- | Generate an expression renaming environment from a pattern. This -- ignores type parameters that can be bound by the pattern. -- | The naming environment for a single module. This is the mapping from -- unqualified internal names to fully qualified names. -- | The naming environment for a single declaration, unqualified. This is -- meanat to be used for things like where clauses. instance Show NameOrigin instance Show EName instance Show TName instance Show NamingEnv instance BindsNames Decl instance BindsNames Module instance BindsNames Pattern instance BindsNames TParam instance BindsNames Bind instance BindsNames Match instance BindsNames IfaceDecls instance BindsNames Iface instance BindsNames Schema instance BindsNames a => BindsNames [a] instance BindsNames a => BindsNames (Maybe a) instance BindsNames NamingEnv instance Monoid NamingEnv instance HasQName EName instance HasQName TName instance PP NameOrigin -- | 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 removePatterns :: RemovePatterns t => t -> (t, [Error]) data Error MultipleSignatures :: QName -> [Located Schema] -> Error SignatureNoBind :: (Located QName) -> Schema -> Error PragmaNoBind :: (Located QName) -> Pragma -> Error instance Show Error instance PP Error instance Monad NoPatM instance Applicative NoPatM instance Functor NoPatM instance RemovePatterns [Decl] instance RemovePatterns Module instance RemovePatterns Expr instance RemovePatterns Program -- | Utility functions that are also useful for translating programs from -- previous Cryptol versions. module Cryptol.Parser.Utils translateExprToNumT :: Expr -> Maybe Type module Cryptol.Parser parseModule :: Config -> String -> Either ParseError Module parseProgram :: Layout -> String -> Either ParseError Program parseProgramWith :: Config -> String -> Either ParseError Program parseExpr :: String -> Either ParseError Expr parseExprWith :: Config -> String -> Either ParseError Expr parseDecl :: String -> Either ParseError Decl parseDeclWith :: Config -> String -> Either ParseError Decl parseDecls :: String -> Either ParseError [Decl] parseDeclsWith :: Config -> String -> Either ParseError [Decl] parseLetDecl :: String -> Either ParseError Decl parseLetDeclWith :: Config -> String -> Either ParseError Decl parseRepl :: String -> Either ParseError ReplInput parseReplWith :: Config -> String -> Either ParseError ReplInput parseSchema :: String -> Either ParseError Schema parseSchemaWith :: Config -> String -> Either ParseError Schema parseModName :: String -> Maybe ModName data ParseError HappyError :: FilePath -> Position -> (Maybe Token) -> ParseError HappyErrorMsg :: Range -> String -> 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 removeIncludes :: Program -> IO (Either [IncludeError] Program) removeIncludesModule :: Module -> IO (Either [IncludeError] Module) data IncludeError IncludeFailed :: (Located FilePath) -> IncludeError IncludeParseError :: ParseError -> IncludeError IncludeCycle :: [Located FilePath] -> IncludeError ppIncludeError :: IncludeError -> Doc instance Show IncludeError instance Monad NoIncM instance Applicative NoIncM instance Functor NoIncM 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 -> NamingEnv -- | Throw errors for any names that overlap in a rewrite environment. checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning]) class Rename a rename :: Rename a => a -> RenameM a runRenamer :: NamingEnv -> RenameM a -> (Either [RenamerError] a, [RenamerWarning]) data RenamerError -- | Multiple imported symbols contain this name MultipleSyms :: (Located QName) -> [NameOrigin] -> RenamerError -- | Expression name is not bound to any definition UnboundExpr :: (Located QName) -> RenamerError -- | Type name is not bound to any definition UnboundType :: (Located QName) -> RenamerError -- | An environment has produced multiple overlapping symbols OverlappingSyms :: [NameOrigin] -> RenamerError -- | When a value is expected from the naming environment, but one or more -- types exist instead. ExpectedValue :: (Located QName) -> RenamerError -- | When a type is missing from the naming environment, but one or more -- values exist with the same name. ExpectedType :: (Located QName) -> RenamerError data RenamerWarning SymbolShadowed :: NameOrigin -> [NameOrigin] -> RenamerWarning instance Show RenamerError instance Show RenamerWarning instance Show Out instance Rename TySyn instance Rename Match instance Rename TypeInst instance Rename Expr instance Rename Pattern instance Rename Bind instance Rename Pragma instance Rename Type instance Rename Prop instance Rename Schema instance Rename Newtype instance Rename Decl instance Rename a => Rename (TopLevel a) instance Rename TopDecl instance Rename Module instance Rename a => Rename (Named a) instance Rename a => Rename (Located a) instance Rename a => Rename (Maybe a) instance Rename a => Rename [a] instance Monad RenameM instance Applicative RenameM instance Functor RenameM instance Monoid Out instance PP RenamerWarning instance PP RenamerError -- | This module contains types used during type inference. module Cryptol.TypeCheck.InferTypes -- | The types of variables in the environment. data VarType -- | Known type ExtVar :: Schema -> VarType -- | Part of current SCC CurSCC :: Expr -> Type -> VarType newtype Goals Goals :: (TypeMap Goal) -> Goals emptyGoals :: Goals nullGoals :: Goals -> Bool fromGoals :: Goals -> [Goal] insertGoal :: Goal -> Goals -> Goals -- | Something that we need to find evidence for. data Goal Goal :: ConstraintSource -> Range -> Prop -> Goal -- | With 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 :: LQName -> [TParam] -> [Prop] -> [Goal] -> DelayedCt -- | Signature that gave rise to this constraint dctSource :: DelayedCt -> LQName dctForall :: DelayedCt -> [TParam] dctAsmps :: DelayedCt -> [Prop] dctGoals :: DelayedCt -> [Goal] data Solved -- | Solved, assumeing the sub-goals. Solved :: (Maybe Subst) -> [Goal] -> Solved -- | We could not solved the goal. Unsolved :: Solved -- | The goal can never be solved Unsolvable :: Solved data Warning DefaultingKind :: TParam -> Kind -> Warning DefaultingWildType :: Kind -> Warning DefaultingTo :: Doc -> 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 resut (which should not be of the -- form _ -> _) TooManyTypeParams :: Int -> Kind -> Error -- | Type-synonym, number of extra params TooManyTySynParams :: QName -> Int -> Error -- | Type-synonym, number of missing params TooFewTySynParams :: QName -> Int -> Error -- | Type parameters with the same name (in definition) RepeatedTyParams :: [TParam] -> Error -- | Multiple definitions for the same name RepeatedDefinitions :: QName -> [Range] -> Error -- | The type synonym declarations are recursive RecursiveTypeDecls :: [LQName] -> Error -- | Use of a type synonym that was not defined UndefinedTypeSynonym :: QName -> Error -- | Use of a variable that was not defined UndefinedVariable :: QName -> Error -- | Attempt to explicitly instantiate a non-existent param. UndefinedTypeParam :: QName -> Error -- | Multiple definitions for the same type parameter MultipleTypeParamDefs :: QName -> [Range] -> 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 UnsolvedGoal :: Goal -> Error -- | A constraint (with context) that we could not solve UnsolvedDelcayedCt :: 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 -> [TVar] -> Error -- | Quantified type variables (of kind *) needs to match the given type, -- so it does not work for all types. NotForAll :: TVar -> Type -> Error -- | The given constraint causes the signature of the function to be -- not-satisfiable. UnusableFunction :: QName -> Prop -> Error -- | Too many positional type arguments, in an explicit type instantiation TooManyPositionalTypeParams :: Error CannotMixPositionalAndNamedTypeParams :: Error AmbiguousType :: [QName] -> Error -- | 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 expreesion 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 data TyFunName UserTyFun :: QName -> TyFunName BuiltInTyFun :: TFun -> TyFunName -- | For use in error messages cppKind :: Kind -> Doc addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc ppUse :: Expr -> Doc instance [safe] Show Warning instance [safe] Show TyFunName instance [safe] Show ConstraintSource instance [safe] Show Goal instance [safe] Show Solved instance [safe] Show DelayedCt instance [safe] Show Error instance [safe] Show HasGoal instance [safe] Show Goals instance [safe] PP Solved instance [safe] PP (WithNames DelayedCt) instance [safe] PP (WithNames Goal) instance [safe] PP ConstraintSource instance [safe] PP (WithNames Error) instance [safe] PP (WithNames Warning) instance [safe] PP Error instance [safe] PP Warning instance [safe] TVars DelayedCt instance [safe] TVars HasGoal instance [safe] TVars Goal instance [safe] TVars Goals instance [safe] FVS DelayedCt instance [safe] FVS Goal instance [safe] FVS Error instance [safe] TVars Error instance [safe] FVS Warning instance [safe] TVars Warning instance [safe] TVars ConstraintSource instance [safe] PP TyFunName module Cryptol.TypeCheck.Monad -- | Information needed for type inference. data InferInput InferInput :: Range -> Map QName Schema -> Map QName TySyn -> Map QName Newtype -> NameSeeds -> Bool -> InferInput -- | Location of program source inpRange :: InferInput -> Range -- | Variables that are in scope inpVars :: InferInput -> Map QName Schema -- | Type synonyms that are in scope inpTSyns :: InferInput -> Map QName TySyn -- | Newtypes in scope inpNewtypes :: InferInput -> Map QName Newtype -- | Private state of type-checker inpNameSeeds :: InferInput -> NameSeeds -- | Should local bindings without signatures be monomorphized? inpMonoBinds :: InferInput -> Bool -- | This is used for generating various names. data NameSeeds NameSeeds :: !Int -> !Int -> NameSeeds seedTVar :: NameSeeds -> !Int seedGoal :: NameSeeds -> !Int -- | The initial seeds, used when checking a fresh program. nameSeeds :: NameSeeds -- | 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 -> a -> InferOutput a runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) newtype InferM a IM :: ReaderT RO (StateT RW IO) a -> InferM a unIM :: InferM a -> ReaderT RO (StateT RW IO) a data DefLoc IsLocal :: DefLoc IsExternal :: DefLoc -- | Read-only component of the monad. data RO RO :: Range -> Map QName VarType -> [TParam] -> Map QName (DefLoc, TySyn) -> Map QName (DefLoc, Newtype) -> Map Int (Expr -> Expr) -> Bool -> RO -- | Source code being analysed iRange :: RO -> Range -- | Type of variable that are in scope iVars :: RO -> Map QName VarType -- | Type variable that are in scope iTVars :: RO -> [TParam] -- | Type synonyms that are in scope iTSyns :: RO -> Map QName (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 QName (DefLoc, Newtype) -- | 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 -- | Read-write component of the monad. data RW RW :: ![(Range, Error)] -> ![(Range, Warning)] -> !Subst -> [Map QName Type] -> Map Int (Expr -> Expr) -> !NameSeeds -> !Goals -> ![HasGoal] -> 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 QName 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] 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 () 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]) -- | 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 () newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a -- | Generate a new name for a goal. newGoalName :: InferM Int -- | Generate a new free type variable. newTVar :: Doc -> Kind -> InferM TVar -- | Generate a new free type variable that depends on these additional -- type parameters. newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar -- | Generate a new free type variable. newTParam :: Maybe QName -> Kind -> InferM TParam -- | Generate an unknown type. The doc is a note about what is this type -- about. newType :: Doc -> 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 -- | Get the substitution that we have accumulated so far. getSubst :: InferM Subst -- | Add to the accumulated substitution. 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 :: QName -> 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. lookupTVar :: QName -> InferM (Maybe Type) -- | Lookup the definition of a type synonym. lookupTSyn :: QName -> InferM (Maybe TySyn) -- | Lookup the definition of a newtype lookupNewtype :: QName -> InferM (Maybe Newtype) -- | 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 :: QName -> Kind -> InferM Type -- | Returns the type synonyms that are currently in scope. getTSyns :: InferM (Map QName (DefLoc, TySyn)) -- | Returns the newtype declarations that are in scope. getNewtypes :: InferM (Map QName (DefLoc, Newtype)) -- | Get the set of bound type variables that are in scope. getTVars :: InferM (Set QName) -- | Return the keys of the bound variables that are in scope. getBoundInScope :: InferM (Set TVar) -- | 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 -> QName -> 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 -- | The sub-computation is performed with the given variable in scope. withVarType :: QName -> VarType -> InferM a -> InferM a withVarTypes :: [(QName, VarType)] -> InferM a -> InferM a withVar :: QName -> Schema -> InferM a -> InferM a -- | The sub-computation is performed with the given variables in scope. withMonoType :: (QName, Located Type) -> InferM a -> InferM a -- | The sub-computation is performed with the given variables in scope. withMonoTypes :: Map QName (Located Type) -> InferM a -> InferM a -- | The sub-computation is performed with the given type synonyms and -- variables in scope. withDecls :: ([TySyn], Map QName 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 newtype KindM a KM :: ReaderT KRO (StateT KRW InferM) a -> KindM a unKM :: KindM a -> ReaderT KRO (StateT KRW InferM) a data KRO KRO :: Map QName Type -> Bool -> KRO -- | lazy map, with tyvars. lazyTVars :: KRO -> Map QName Type -- | are type-wild cards allowed? allowWild :: KRO -> Bool data KRW KRW :: Map QName Kind -> KRW -- | kinds of (known) vars. typeParams :: KRW -> Map QName Kind -- | The arguments to this function are as follows: -- -- (type param. name, kind signature (opt.), a type representing the -- param) -- -- The type representing the parameter is just a thunk that we should not -- force. The reason is that the type depnds on the kind of parameter, -- 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 :: Bool -> [(QName, Maybe Kind, Type)] -> KindM a -> InferM (a, Map QName Kind) -- | This is what's returned when we lookup variables during kind checking. data LkpTyVar -- | Locally bound variable. TLocalVar :: Type -> (Maybe Kind) -> LkpTyVar -- | An outer binding. TOuterVar :: Type -> LkpTyVar -- | Check if a name refers to a type variable. kLookupTyVar :: QName -> KindM (Maybe LkpTyVar) -- | Are type wild-cards OK in this context? kWildOK :: KindM Bool -- | Reports an error. kRecordError :: Error -> KindM () kRecordWarning :: Warning -> KindM () -- | Generate a fresh unification variable of the given kind. kNewType :: Doc -> Kind -> KindM Type -- | Lookup the definition of a type synonym. kLookupTSyn :: QName -> KindM (Maybe TySyn) -- | Lookup the definition of a newtype. kLookupNewtype :: QName -> KindM (Maybe Newtype) kExistTVar :: QName -> 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 :: QName -> 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 [safe] Show NameSeeds instance [safe] Show InferInput instance [safe] Show a => Show (InferOutput a) instance [safe] Monad KindM instance [safe] Applicative KindM instance [safe] Functor KindM instance [safe] MonadFix InferM instance [safe] Monad InferM instance [safe] Applicative InferM instance [safe] Functor InferM module Cryptol.TypeCheck.Depends data TyDecl TS :: TySyn -> TyDecl NT :: Newtype -> TyDecl -- | Check for duplicate and recursive type synonyms. Returns the -- type-synonyms in dependecy order. orderTyDecls :: [TyDecl] -> InferM [TyDecl] -- | Associate type signatures with bindings and order bindings by -- dependency. orderBinds :: [Bind] -> [SCC Bind] class FromDecl d toBind :: FromDecl d => d -> Maybe Bind 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, [QName], [QName])] -> [SCC a] -- | Combine a bunch of definitions into a single map. Here we check that -- each name is defined only onces. combineMaps :: [Map QName (Located a)] -> InferM (Map QName (Located a)) -- | Combine a bunch of definitions into a single map. Here we check that -- each name is defined only onces. combine :: [(QName, Located a)] -> InferM (Map QName (Located a)) -- | Identify multiple occurances of something. duplicates :: Ord a => [Located a] -> [(a, [Range])] instance [safe] FromDecl Decl instance [safe] FromDecl TopDecl module Cryptol.TypeCheck.Instantiate instantiateWith :: Expr -> Schema -> [Located (Maybe QName, Type)] -> InferM (Expr, Type) -- | This module contains machinery to reason about ordering of variables, -- their finiteness, and their possible intervals. module Cryptol.TypeCheck.Solver.FinOrd data OrdFacts -- | Possible outcomes, when asserting a fact. data AssertResult -- | We added a new fact OrdAdded :: OrdFacts -> AssertResult -- | We already knew this OrdAlreadyKnown :: AssertResult -- | Only if the two types are equal OrdImprove :: Type -> Type -> AssertResult -- | The fact is known to be false OrdImpossible :: AssertResult -- | We could not perform opertaion. OrdCannot :: AssertResult noFacts :: OrdFacts addFact :: IsFact t => t -> OrdFacts -> AssertResult -- | Query if the one type is known to be smaller than, or equal to, the -- other. Assumes that the type is simple (i.e., no type functions). isKnownLeq :: OrdFacts -> Type -> Type -> Bool -- | Compute an interval, that we know definately contains the given type. -- Assumes that the type is normalized (i.e., no type functions). knownInterval :: OrdFacts -> Type -> Interval ordFactsToGoals :: OrdFacts -> [Goal] ordFactsToProps :: OrdFacts -> [Prop] -- | Render facts in dot notation. The boolean says if we want the -- arrows to point up. dumpDot :: Bool -> OrdFacts -> String dumpDoc :: OrdFacts -> Doc -- | Add a `(>=)` or fin goal into the model. Assumes that the -- types are normalized (i.e., no type functions). class IsFact t factProp :: IsFact t => t -> Prop factChangeProp :: IsFact t => t -> Prop -> t factSource :: IsFact t => t -> EdgeSrc instance [safe] Show OrdTerms instance [safe] Show EdgeSrc instance [safe] Eq Nat'' instance [safe] Ord Nat'' instance [safe] Show Nat'' instance [safe] Eq NumType instance [safe] Ord NumType instance [safe] Show NumType instance [safe] Show Edge instance [safe] Show Edges instance [safe] Show OrdFacts instance [safe] Show AssertResult instance [safe] Ord Edge instance [safe] Eq Edge instance [safe] IsFact Prop instance [safe] IsFact Goal -- | We define the behavior of Cryptol's type-level functions on integers. module Cryptol.TypeCheck.Solver.Eval -- | Collect fin and simple <= constraints in the ord -- model Returns Left if we find a goal which is incompatible with -- the others. Otherwise, we return Right with a model, and the -- remaining (i.e., the non-order related) properties. -- -- These sorts of facts are quite useful during type simplification, -- because they provide information which potentially useful for -- cancellation (e.g., this variables is finite and not 0) assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop]) -- | This returns order properties that are implied by the give property. -- It is important that the returned properties are propoer ordering -- properties (i.e., addFact will not return OrdCannot). derivedOrd :: OrdFacts -> Prop -> [Prop] isSimpleType :: Type -> Bool simpType :: OrdFacts -> Type -> Type reorderArgs :: TFun -> [Type] -> [Type] commuteArgs :: [Type] -> [Type] evalTFun :: OrdFacts -> TFun -> [Type] -> Maybe Type typeInterval :: OrdFacts -> Type -> Interval typeKnownLeq :: OrdFacts -> Type -> Type -> Bool typeKnownFin :: OrdFacts -> Type -> Bool tfAdd :: OrdFacts -> Type -> Type -> Maybe Type -- | tfSub x y = Just z iff z is the unique value such -- that tfAdd y z = Just x tfSub :: OrdFacts -> Type -> Type -> Maybe Type -- | It is important that the 0 rules come before the Inf ones tfMul :: OrdFacts -> Type -> Type -> Maybe Type tfDiv :: OrdFacts -> Type -> Type -> Maybe Type tfMod :: OrdFacts -> Type -> Type -> Maybe Type tfMin :: OrdFacts -> Type -> Type -> Maybe Type tfMax :: OrdFacts -> Type -> Type -> Maybe Type tfExp :: OrdFacts -> Type -> Type -> Maybe Type -- | Rounds up lg2 x = Just y, if y is the smallest -- number such that x <= 2 ^ y tfLg2 :: OrdFacts -> Type -> Maybe Type -- | XXX: width and lg2 are almost the same! width n -- == lg2 (n + 1) tfWidth :: OrdFacts -> Type -> Maybe Type tfLenFromThen :: OrdFacts -> Type -> Type -> Type -> Maybe Type tfLenFromThenTo :: OrdFacts -> Type -> Type -> Type -> Maybe Type toNat' :: Type -> Maybe Nat' fromNat' :: Nat' -> Type oneOrMore :: OrdFacts -> Type -> Bool twoOrMore :: OrdFacts -> Type -> Bool -- | Solver code that does not depend on the type inference monad. module Cryptol.TypeCheck.Solver.Numeric -- | Try to perform a single step of simplification for a numeric goal. We -- assume that the substitution has been applied to the goal. numericStep :: OrdFacts -> Goal -> Solved simpFin :: OrdFacts -> Prop -> Maybe [Prop] -- | Collect fin and <= constraints in the ord model -- Returns (new model, bad goals, other goals). "bad goals" are goals -- that are incompatible with the model "other goals" are ones that are -- not "<=" or "fin" goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal]) module Cryptol.TypeCheck.Defaulting tryDefault :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning]) tryDefaultWith :: OrdFacts -> [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 -- resaulting types should satisfy the constraints of the schema. defaultExpr :: Range -> Expr -> Schema -> Maybe ([(TParam, Type)], Expr) -- | Solving class constraints. module Cryptol.TypeCheck.Solver.Class -- | Solve class constraints. classStep :: Goal -> Solved -- | Add propositions that are implied by the given one. The result -- contains the orignal proposition, and maybe some more. expandProp :: Prop -> [Prop] module Cryptol.TypeCheck.Solver.Selector -- | Solve has-constraints. tryHasGoal :: HasGoal -> InferM () module Cryptol.TypeCheck.Solver.Smtlib simpDelayed :: [TParam] -> OrdFacts -> [Prop] -> [Goal] -> IO [Goal] instance Eq SMTResult instance Show SMTResult module Cryptol.TypeCheck.Solve simplifyAllConstraints :: InferM () proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst -- | Collect fin and simple <= constraints in the ord -- model Returns Left if we find a goal which is incompatible with -- the others. Otherwise, we return Right with a model, and the -- remaining (i.e., the non-order related) properties. -- -- These sorts of facts are quite useful during type simplification, -- because they provide information which potentially useful for -- cancellation (e.g., this variables is finite and not 0) assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop]) checkTypeFunction :: TFun -> [Type] -> [Prop] module Cryptol.TypeCheck.Kind checkType :: Type -> Maybe Kind -> InferM Type -- | Check a type signature. checkSchema :: Schema -> InferM (Schema, [Goal]) -- | Check a newtype declaration. XXX: Do something with constraints. checkNewtype :: Newtype -> InferM Newtype -- | Check a type-synonym declaration. checkTySyn :: TySyn -> InferM TySyn -- | Assumes that the NoPat pass has been run. module Cryptol.TypeCheck.Infer inferModule :: Module -> InferM Module desugarLiteral :: Bool -> Literal -> InferM Expr -- | Infer the type of an expression with an explicit instantiation. appTys :: Expr -> [Located (Maybe QName, Type)] -> Type -> InferM Expr inferTyParam :: TypeInst -> InferM (Located (Maybe QName, Type)) checkTypeOfKind :: Type -> Kind -> InferM Type -- | We use this when we want to ensure that the expr has exactly -- (syntactically) the given type. inferE :: Doc -> Expr -> InferM (Expr, Type) -- | Infer the type of an expression, and translate it to a fully -- elaborated core term. checkE :: Expr -> Type -> InferM Expr expectSeq :: Type -> InferM (Type, Type) expectTuple :: Int -> Type -> InferM [Type] expectRec :: [Named a] -> Type -> InferM [(Name, a, Type)] expectFin :: Int -> Type -> InferM () expectFun :: Int -> Type -> InferM ([Type], Type) checkHasType :: Expr -> Type -> Type -> InferM Expr checkFun :: Doc -> [Pattern] -> Expr -> Type -> InferM Expr -- | The type the is the smallest of all smallest :: [Type] -> InferM Type checkP :: Doc -> Pattern -> Type -> InferM (Located QName) -- | Infer the type of a pattern. Assumes that the pattern will be just a -- variable. inferP :: Doc -> Pattern -> InferM (QName, Located Type) -- | Infer the type of one match in a list comprehension. inferMatch :: Match -> InferM (Match, QName, Located Type, Type) -- | Infer the type of one arm of a list comprehension. inferCArm :: Int -> [Match] -> InferM ([Match], Map QName (Located Type), Type) -- | 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] -> InferM [Decl] -- | Come up with a type for recursive calls to a function, and decide how -- we are going to be checking the binding. Returns: (Name, type or -- schema, computation to check binding) -- -- The exprMap is a thunk where we can lookup the final -- expressions and we should be careful not to force it. guessType :: Map QName Expr -> Bind -> InferM ((QName, VarType), Either (InferM Decl) (InferM Decl)) -- | Try to evaluate the inferred type of a mono-binding simpMonoBind :: OrdFacts -> Decl -> Decl -- | The inputs should be declarations with monomorphic types (i.e., of the -- form `Forall [] [] t`). generalize :: [Decl] -> [Goal] -> InferM [Decl] checkMonoB :: Bind -> Type -> InferM Decl checkSigB :: Bind -> (Schema, [Goal]) -> InferM Decl inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a tcPanic :: String -> [String] -> a module Cryptol.TypeCheck tcModule :: Module -> InferInput -> IO (InferOutput Module) tcExpr :: Expr -> InferInput -> IO (InferOutput (Expr, Schema)) tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup]) -- | Information needed for type inference. data InferInput InferInput :: Range -> Map QName Schema -> Map QName TySyn -> Map QName Newtype -> NameSeeds -> Bool -> InferInput -- | Location of program source inpRange :: InferInput -> Range -- | Variables that are in scope inpVars :: InferInput -> Map QName Schema -- | Type synonyms that are in scope inpTSyns :: InferInput -> Map QName TySyn -- | Newtypes in scope inpNewtypes :: InferInput -> Map QName Newtype -- | Private state of type-checker inpNameSeeds :: InferInput -> NameSeeds -- | Should local bindings without signatures be monomorphized? inpMonoBinds :: InferInput -> Bool -- | 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 -> a -> InferOutput a -- | This is used for generating various names. data NameSeeds -- | The initial seeds, used when checking a fresh program. 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 resut (which should not be of the -- form _ -> _) TooManyTypeParams :: Int -> Kind -> Error -- | Type-synonym, number of extra params TooManyTySynParams :: QName -> Int -> Error -- | Type-synonym, number of missing params TooFewTySynParams :: QName -> Int -> Error -- | Type parameters with the same name (in definition) RepeatedTyParams :: [TParam] -> Error -- | Multiple definitions for the same name RepeatedDefinitions :: QName -> [Range] -> Error -- | The type synonym declarations are recursive RecursiveTypeDecls :: [LQName] -> Error -- | Use of a type synonym that was not defined UndefinedTypeSynonym :: QName -> Error -- | Use of a variable that was not defined UndefinedVariable :: QName -> Error -- | Attempt to explicitly instantiate a non-existent param. UndefinedTypeParam :: QName -> Error -- | Multiple definitions for the same type parameter MultipleTypeParamDefs :: QName -> [Range] -> 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 UnsolvedGoal :: Goal -> Error -- | A constraint (with context) that we could not solve UnsolvedDelcayedCt :: 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 -> [TVar] -> Error -- | Quantified type variables (of kind *) needs to match the given type, -- so it does not work for all types. NotForAll :: TVar -> Type -> Error -- | The given constraint causes the signature of the function to be -- not-satisfiable. UnusableFunction :: QName -> Prop -> Error -- | Too many positional type arguments, in an explicit type instantiation TooManyPositionalTypeParams :: Error CannotMixPositionalAndNamedTypeParams :: Error AmbiguousType :: [QName] -> Error data Warning DefaultingKind :: TParam -> Kind -> Warning DefaultingWildType :: Kind -> Warning DefaultingTo :: Doc -> Type -> Warning ppWarning :: (Range, Warning) -> Doc ppError :: (Range, Error) -> Doc module Cryptol.ModuleSystem.Env data ModuleEnv ModuleEnv :: LoadedModules -> NameSeeds -> EvalEnv -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Bool -> ModuleEnv meLoadedModules :: ModuleEnv -> LoadedModules meNameSeeds :: ModuleEnv -> NameSeeds meEvalEnv :: ModuleEnv -> EvalEnv meFocusedModule :: ModuleEnv -> Maybe ModName meSearchPath :: ModuleEnv -> [FilePath] meDynEnv :: ModuleEnv -> DynamicEnv meMonoBinds :: ModuleEnv -> !Bool 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. -- -- This could really do with some better error handling, just returning -- mempty when one of the imports fails isn't really desirable. focusedEnv :: ModuleEnv -> IfaceDecls -- | Produce an ifaceDecls that represents the internal environment of the -- module, used for typechecking. qualifiedEnv :: ModuleEnv -> IfaceDecls loadModuleEnv :: (Import -> Iface -> Iface) -> ModuleEnv -> Maybe (Iface, IfaceDecls) -- | Invariant: All the dependencies of any module m must precede -- m in the list. newtype LoadedModules LoadedModules :: [LoadedModule] -> LoadedModules getLoadedModules :: LoadedModules -> [LoadedModule] data LoadedModule LoadedModule :: ModName -> FilePath -> Iface -> Module -> LoadedModule lmName :: LoadedModule -> ModName lmFilePath :: LoadedModule -> FilePath lmInterface :: LoadedModule -> Iface lmModule :: LoadedModule -> Module isLoaded :: ModName -> LoadedModules -> Bool lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule addLoadedModule :: FilePath -> Module -> LoadedModules -> LoadedModules removeLoadedModule :: FilePath -> 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 Show LoadedModule instance Show LoadedModules instance Monoid DynamicEnv instance Monoid LoadedModules module Cryptol.ModuleSystem.Monad data ImportSource FromModule :: ModName -> ImportSource FromImport :: (Located Import) -> 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 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 data ModuleWarning TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning RenamerWarnings :: [RenamerWarning] -> ModuleWarning warn :: [ModuleWarning] -> ModuleM () typeCheckWarnings :: [(Range, Warning)] -> ModuleM () renamerWarnings :: [RenamerWarning] -> ModuleM () data RO RO :: [ImportSource] -> RO roLoading :: RO -> [ImportSource] emptyRO :: 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 => ModuleEnv -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning]) type ModuleM = ModuleT IO runModuleM :: 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 () isLoaded :: ModName -> ModuleM Bool loadingImport :: Located Import -> ModuleM a -> ModuleM a loadingModule :: 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 getNameSeeds :: ModuleM NameSeeds getMonoBinds :: ModuleM Bool setMonoBinds :: Bool -> ModuleM () setNameSeeds :: NameSeeds -> ModuleM () -- | Remove a module from the set of loaded module, by its path. unloadModule :: FilePath -> ModuleM () loadedModule :: FilePath -> Module -> ModuleM () modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM () getEvalEnv :: ModuleM EvalEnv 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 IfaceDecls getQualifiedEnv :: ModuleM IfaceDecls getDynEnv :: ModuleM DynamicEnv setDynEnv :: DynamicEnv -> ModuleM () instance Show ImportSource instance Show ModuleError instance Show ModuleWarning instance MonadT ModuleT instance Monad m => Monad (ModuleT m) instance Monad m => Applicative (ModuleT m) instance Monad m => Functor (ModuleT m) instance PP ModuleWarning instance PP ModuleError instance PP ImportSource instance Eq ImportSource module Cryptol.ModuleSystem.Base rename :: Rename a => NamingEnv -> a -> ModuleM a -- | Rename a module in the context of its imported modules. renameModule :: Module -> ModuleM Module -- | Rename an expression in the context of the focused module. renameExpr :: Expr -> ModuleM Expr -- | Rename declarations in the context of the focused module. renameDecls :: (Rename d, FromDecl d) => [d] -> ModuleM [d] -- | Run the noPat pass. noPat :: RemovePatterns a => a -> ModuleM a parseModule :: FilePath -> ModuleM Module -- | Load a module by its path. loadModuleByPath :: FilePath -> ModuleM Module -- | Load the module specified by an import. loadImport :: Located Import -> ModuleM () -- | Load dependencies, typecheck, and add to the eval environment. loadModule :: FilePath -> Module -> ModuleM Module -- | Rewrite an import declaration to be of the form: -- -- 
--   import foo as foo [ [hiding] (a,b,c) ]
--
fullyQualified :: Import -> Import -- | Process the interface specified by an import. importIface :: Import -> ModuleM Iface -- | Load a series of interfaces, merging their public interfaces. importIfaces :: [Import] -> ModuleM IfaceDecls 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 preludeName :: ModName -- | Add the prelude to the import list if it's not already mentioned. addPrelude :: Module -> Module -- | Load the dependencies of a module into the environment. loadDeps :: Module -> ModuleM () -- | Typecheck a single expression. checkExpr :: Expr -> ModuleM (Expr, Schema) -- | Typecheck a group of declarations. checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleM [DeclGroup] -- | Typecheck a module. checkModule :: Module -> ModuleM Module type TCAction i o = i -> InferInput -> IO (InferOutput o) typecheck :: HasLoc i => TCAction i o -> i -> IfaceDecls -> ModuleM o -- | Process a list of imports, producing an aggregate interface suitable -- for use when typechecking. importIfacesTc :: [Import] -> ModuleM IfaceDecls -- | Generate input for the typechecker. genInferInput :: Range -> IfaceDecls -> ModuleM InferInput evalExpr :: Expr -> ModuleM Value evalDecls :: [DeclGroup] -> ModuleM () module Cryptol.ModuleSystem data ModuleEnv ModuleEnv :: LoadedModules -> NameSeeds -> EvalEnv -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Bool -> ModuleEnv meLoadedModules :: ModuleEnv -> LoadedModules meNameSeeds :: ModuleEnv -> NameSeeds meEvalEnv :: ModuleEnv -> EvalEnv meFocusedModule :: ModuleEnv -> Maybe ModName meSearchPath :: ModuleEnv -> [FilePath] meDynEnv :: ModuleEnv -> DynamicEnv meMonoBinds :: ModuleEnv -> !Bool 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 data ModuleWarning TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning RenamerWarnings :: [RenamerWarning] -> ModuleWarning type ModuleCmd a = 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 Module -- | Load the given parsed module. loadModule :: FilePath -> Module -> ModuleCmd Module -- | Check the type of an expression. checkExpr :: Expr -> ModuleCmd (Expr, Schema) -- | Evaluate an expression. evalExpr :: Expr -> ModuleCmd Value -- | Typecheck declarations. checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleCmd [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. -- -- This could really do with some better error handling, just returning -- mempty when one of the imports fails isn't really desirable. focusedEnv :: ModuleEnv -> IfaceDecls -- | The resulting interface generated by a module that has been -- typechecked. data Iface Iface :: ModName -> IfaceDecls -> IfaceDecls -> Iface ifModName :: Iface -> ModName ifPublic :: Iface -> IfaceDecls ifPrivate :: Iface -> IfaceDecls data IfaceDecls IfaceDecls :: Map QName [IfaceTySyn] -> Map QName [IfaceNewtype] -> Map QName [IfaceDecl] -> IfaceDecls ifTySyns :: IfaceDecls -> Map QName [IfaceTySyn] ifNewtypes :: IfaceDecls -> Map QName [IfaceNewtype] ifDecls :: IfaceDecls -> Map QName [IfaceDecl] -- | Generate an Iface from a typechecked module. genIface :: Module -> Iface type IfaceTySyn = TySyn data IfaceDecl IfaceDecl :: QName -> Schema -> [Pragma] -> IfaceDecl ifDeclName :: IfaceDecl -> QName ifDeclSig :: IfaceDecl -> Schema ifDeclPragmas :: IfaceDecl -> [Pragma] module Cryptol.Transform.Specialize -- | A QName should have an entry in the SpecCache iff it is specializable. -- Each QName starts out with an empty TypesMap. type SpecCache = Map QName (Decl, TypesMap (QName, 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 QName (TypesMap QName)) -- | 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 QName (TypesMap QName)) specializeConst :: Expr -> SpecM Expr destEProofApps :: Expr -> (Expr, Int) destETApps :: Expr -> (Expr, [Type]) destEProofAbs :: Expr -> ([Prop], Expr) destETAbs :: Expr -> ([TParam], Expr) freshName :: QName -> [Type] -> SpecM QName matchingBoundNames :: (Maybe ModName) -> SpecM [String] reifyName :: Name -> [Type] -> String 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] allPublicQNames :: ModuleEnv -> [QName] traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c) module Cryptol.Symbolic.Prims traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) evalECon :: ECon -> Value selectV :: (Integer -> Value) -> Value -> Value replicateV :: Integer -> Value -> Value nth :: a -> [a] -> Int -> a nthV :: Value -> Value -> Integer -> Value mapV :: Bool -> (Value -> Value) -> Value -> Value catV :: Value -> Value -> Value dropV :: Integer -> Value -> Value takeV :: Integer -> Value -> Value -- | Make a numeric constant. { val, bits } (fin val, fin bits, bits >= -- width val) => [bits] ecDemoteV :: Value -- | An easy-to-use alternative representation for type TValue. data TypeVal TVBit :: TypeVal TVSeq :: Int -> TypeVal -> TypeVal TVStream :: TypeVal -> TypeVal TVTuple :: [TypeVal] -> TypeVal TVRecord :: [(Name, TypeVal)] -> TypeVal TVFun :: TypeVal -> TypeVal -> TypeVal toTypeVal :: TValue -> TypeVal type Binary = TValue -> Value -> Value -> Value type Unary = TValue -> Value -> Value -- | Models functions of type `{a} (Arith a) => a -> a -> a` arithBinary :: (SWord -> SWord -> SWord) -> Binary -- | Models functions of type `{a} (Arith a) => a -> a` arithUnary :: (SWord -> SWord) -> Unary sExp :: SWord -> SWord -> SWord -- | Ceiling (log_2 x) sLg2 :: SWord -> SWord cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> (Value -> Value -> a -> a) cmpEq :: EqSymbolic a => a -> a -> SBool -> SBool cmpNotEq :: EqSymbolic a => a -> a -> SBool -> SBool cmpLt :: OrdSymbolic a => a -> a -> SBool -> SBool cmpGt :: OrdSymbolic a => a -> a -> SBool -> SBool cmpLtEq :: OrdSymbolic a => a -> a -> SBool -> SBool cmpGtEq :: OrdSymbolic a => a -> a -> SBool -> SBool cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary errorV :: String -> TValue -> Value zeroV :: TValue -> Value -- | Join a sequence of sequences into a single sequence. joinV :: TValue -> TValue -> TValue -> Value -> Value -- | Split implementation. ecSplitV :: Value -- | Split into infinitely many chunks infChunksOf :: Integer -> [a] -> [[a]] -- | Split into finitely many chunks finChunksOf :: Integer -> Integer -> [a] -> [[a]] -- | Merge two values given a binop. This is used for and, or and xor. logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary fromThenV :: Value fromToV :: Value fromThenToV :: Value -- | Add two polynomials addPoly :: [SBool] -> [SBool] -> [SBool] ites :: SBool -> [SBool] -> [SBool] -> [SBool] degree :: [SBool] -> Int mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) idx :: [SBool] -> Int -> SBool divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool]) module Cryptol.Symbolic proverConfigs :: [(String, SMTConfig)] proverNames :: [String] lookupProver :: String -> SMTConfig type SatResult = [(Type, Expr, Value)] -- | 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 allSatSMTResults :: AllSatResult -> [SMTResult] thmSMTResults :: ThmResult -> [SMTResult] satProve :: Bool -> Maybe Int -> (String, Bool, Bool) -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult satProveOffline :: Bool -> Bool -> Bool -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult protectStack :: Bool -> ModuleCmd ProverResult -> ModuleCmd ProverResult parseValues :: [FinType] -> [CW] -> ([Value], [CW]) parseValue :: FinType -> [CW] -> (Value, [CW]) allDeclGroups :: ModuleEnv -> [DeclGroup] data FinType FTBit :: FinType FTSeq :: Int -> FinType -> FinType FTTuple :: [FinType] -> FinType FTRecord :: [(Name, FinType)] -> FinType numType :: Type -> Maybe Int finType :: Type -> Maybe FinType unFinType :: FinType -> Type predArgTypes :: Schema -> Either String [FinType] forallFinType :: FinType -> Symbolic Value existsFinType :: FinType -> Symbolic Value data Env Env :: Map QName Value -> Map TVar TValue -> Bool -> Env envVars :: Env -> Map QName Value envTypes :: Env -> Map TVar TValue envIteSolver :: Env -> Bool emptyEnv :: Bool -> Env -- | Bind a variable in the evaluation environment. bindVar :: (QName, Value) -> Env -> Env -- | Lookup a variable in the environment. lookupVar :: QName -> Env -> Maybe Value -- | Bind a type variable of kind *. bindType :: TVar -> TValue -> Env -> Env -- | Lookup a type variable. lookupType :: TVar -> Env -> Maybe TValue evalExpr :: Env -> Expr -> Value evalType :: Env -> Type -> TValue evalSel :: Selector -> Value -> Value evalDecls :: Env -> [DeclGroup] -> Env evalDeclGroup :: Env -> DeclGroup -> Env evalDecl :: Env -> Decl -> (QName, Value) -- | Make a copy of the given value, building the spine based only on the -- type without forcing the value argument. This lets us avoid strictness -- problems when evaluating recursive definitions. copyBySchema :: Env -> Schema -> Value -> Value copyByType :: Env -> TValue -> Value -> Value -- | Evaluate a comprehension. evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value -- | Turn a list of matches into the final environments for each iteration -- of the branch. branchEnvs :: Env -> [Match] -> [Env] -- | Turn a match into the list of environments it represents. evalMatch :: Env -> Match -> [Env] instance Monoid Env 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 -> 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 :: ModuleError -> REPLException EvalPolyError :: Schema -> REPLException TypeNotTestable :: Type -> REPLException rethrowEvalError :: IO a -> IO a 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 :: QName -> REPL QName getTSyns :: REPL (Map QName TySyn) getNewtypes :: REPL (Map QName Newtype) getVars :: REPL (Map QName IfaceDecl) whenDebug :: REPL () -> REPL () -- | Get visible variable names. getExprNames :: REPL [String] -- | Get visible type signature names. getTypeNames :: REPL [String] getPropertyNames :: REPL [String] data LoadedModule LoadedModule :: Maybe ModName -> FilePath -> LoadedModule -- | Focused module lName :: LoadedModule -> Maybe ModName -- | Focused 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 () setSearchPath :: [FilePath] -> REPL () prependSearchPath :: [FilePath] -> REPL () builtIns :: [(String, (ECon, Schema))] -- | 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 () -> REPL () disableLet :: REPL () enableLet :: REPL () -- | Are let-bindings enabled in this REPL? getLetEnabled :: REPL Bool -- | Update the title updateREPLTitle :: REPL () -- | Set the function that will be called when updating the title setUpdateREPLTitle :: REPL () -> REPL () data EnvVal EnvString :: String -> EnvVal EnvNum :: !Int -> EnvVal EnvBool :: Bool -> EnvVal data OptionDescr OptionDescr :: String -> EnvVal -> (EnvVal -> IO (Maybe String)) -> String -> (EnvVal -> REPL ()) -> OptionDescr optName :: OptionDescr -> String optDefault :: OptionDescr -> EnvVal optCheck :: OptionDescr -> EnvVal -> IO (Maybe String) 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 (Maybe Int) -- | Get the REPL's string-printer getPutStr :: REPL (String -> IO ()) -- | Set the REPL's string-printer setPutStr :: (String -> IO ()) -> REPL () smokeTest :: REPL [Smoke] data Smoke CVC4NotFound :: Smoke instance Typeable REPLException instance Show REPLException instance Show EnvVal instance Show Smoke instance Eq Smoke instance PP Smoke instance PP REPLException instance Exception REPLException instance Monad REPL instance Applicative REPL instance Functor REPL 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 DeclsArg :: (String -> REPL ()) -> CommandBody ExprTypeArg :: (String -> REPL ()) -> CommandBody FilenameArg :: (FilePath -> REPL ()) -> CommandBody OptionArg :: (String -> REPL ()) -> CommandBody ShellArg :: (String -> REPL ()) -> CommandBody NoArg :: (REPL ()) -> CommandBody -- | Parse a line as a command. parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command -- | Run a command. runCommand :: Command -> REPL () -- | 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 () handleCtrlC :: REPL () -- | 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 Eq QCMode instance Show QCMode instance Ord CommandDescr instance Eq CommandDescr instance Show CommandDescr