-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Cryptol: The Language of Cryptography -- -- Cryptol is a domain-specific language for specifying cryptographic -- algorithms. A Cryptol implementation of an algorithm resembles its -- mathematical specification more closely than an implementation in a -- general purpose language. For more, see -- http://www.cryptol.net/. @package cryptol @version 2.2.5 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 GHC.Show.Show Cryptol.Utils.Panic.CryptolPanic instance GHC.Exception.Exception Cryptol.Utils.Panic.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 GHC.Classes.Ord Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.InfNat.Nat' instance GHC.Show.Show Cryptol.TypeCheck.Solver.InfNat.Nat' -- | 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 GHC.Show.Show Cryptol.TypeCheck.Solver.Interval.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 GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.NonLin instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Result instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Prop instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Expr instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.InfNat instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.CrySAT.InfNat instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.CrySAT.InfNat instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.CrySAT.Name instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.CrySAT.Name instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Name instance GHC.Base.Functor Cryptol.TypeCheck.Solver.CrySAT.FM instance GHC.Base.Applicative Cryptol.TypeCheck.Solver.CrySAT.FM instance GHC.Base.Alternative Cryptol.TypeCheck.Solver.CrySAT.FM instance GHC.Base.Monad Cryptol.TypeCheck.Solver.CrySAT.FM instance GHC.Base.MonadPlus Cryptol.TypeCheck.Solver.CrySAT.FM module Cryptol.REPL.Trie -- | Maps string names to values, allowing for partial key matches and -- querying. data Trie a Node :: (Map Char (Trie a)) -> (Maybe a) -> Trie a emptyTrie :: Trie a -- | Insert a value into the Trie. Will call panic if a value -- already exists with that key. insertTrie :: String -> a -> Trie a -> Trie a -- | Return all matches with the given prefix. lookupTrie :: String -> Trie a -> [a] -- | Given a key, return either an exact match for that key, or all matches -- with the given prefix. lookupTrieExact :: String -> Trie a -> [a] -- | Return all of the values from a Trie. leaves :: Trie a -> [a] instance GHC.Show.Show a => GHC.Show.Show (Cryptol.REPL.Trie.Trie a) 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 GHC.Classes.Eq Cryptol.Utils.PP.Assoc instance GHC.Show.Show Cryptol.Utils.PP.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 GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.Position.Located a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.Position.Located a) instance GHC.Show.Show Cryptol.Parser.Position.Range instance GHC.Classes.Eq Cryptol.Parser.Position.Range instance GHC.Show.Show Cryptol.Parser.Position.Position instance GHC.Classes.Ord Cryptol.Parser.Position.Position instance GHC.Classes.Eq Cryptol.Parser.Position.Position instance GHC.Base.Functor Cryptol.Parser.Position.Located instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Position instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Range instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.Position.Located a) instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.Position.Range instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.Position.Located a) instance (Cryptol.Parser.Position.HasLoc a, Cryptol.Parser.Position.HasLoc b) => Cryptol.Parser.Position.HasLoc (a, b) instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc [a] instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.Position.Located a) 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 GHC.Base.Functor Cryptol.Parser.Lexer.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 GHC.Enum.Enum Cryptol.Prims.Syntax.ECon instance GHC.Enum.Bounded Cryptol.Prims.Syntax.ECon instance GHC.Show.Show Cryptol.Prims.Syntax.ECon instance GHC.Classes.Ord Cryptol.Prims.Syntax.ECon instance GHC.Classes.Eq Cryptol.Prims.Syntax.ECon instance GHC.Enum.Enum Cryptol.Prims.Syntax.TFun instance GHC.Enum.Bounded Cryptol.Prims.Syntax.TFun instance GHC.Classes.Ord Cryptol.Prims.Syntax.TFun instance GHC.Classes.Eq Cryptol.Prims.Syntax.TFun instance GHC.Show.Show Cryptol.Prims.Syntax.TFun instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TFun instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.ECon 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 GHC.Show.Show Cryptol.Parser.AST.Program instance GHC.Classes.Eq Cryptol.Parser.AST.Program instance GHC.Show.Show Cryptol.Parser.AST.Module instance GHC.Classes.Eq Cryptol.Parser.AST.Module instance GHC.Show.Show Cryptol.Parser.AST.TopDecl instance GHC.Classes.Eq Cryptol.Parser.AST.TopDecl instance GHC.Show.Show Cryptol.Parser.AST.ReplInput instance GHC.Classes.Eq Cryptol.Parser.AST.ReplInput instance GHC.Show.Show Cryptol.Parser.AST.Bind instance GHC.Classes.Eq Cryptol.Parser.AST.Bind instance GHC.Show.Show Cryptol.Parser.AST.Match instance GHC.Classes.Eq Cryptol.Parser.AST.Match instance GHC.Show.Show Cryptol.Parser.AST.Expr instance GHC.Classes.Eq Cryptol.Parser.AST.Expr instance GHC.Show.Show Cryptol.Parser.AST.Decl instance GHC.Classes.Eq Cryptol.Parser.AST.Decl instance GHC.Show.Show Cryptol.Parser.AST.Schema instance GHC.Classes.Eq Cryptol.Parser.AST.Schema instance GHC.Show.Show Cryptol.Parser.AST.Prop instance GHC.Classes.Eq Cryptol.Parser.AST.Prop instance GHC.Show.Show Cryptol.Parser.AST.TySyn instance GHC.Classes.Eq Cryptol.Parser.AST.TySyn instance GHC.Show.Show Cryptol.Parser.AST.Newtype instance GHC.Classes.Eq Cryptol.Parser.AST.Newtype instance GHC.Show.Show Cryptol.Parser.AST.TypeInst instance GHC.Classes.Eq Cryptol.Parser.AST.TypeInst instance GHC.Show.Show Cryptol.Parser.AST.Pattern instance GHC.Classes.Eq Cryptol.Parser.AST.Pattern instance GHC.Show.Show Cryptol.Parser.AST.Type instance GHC.Classes.Eq Cryptol.Parser.AST.Type instance GHC.Show.Show Cryptol.Parser.AST.TParam instance GHC.Classes.Eq Cryptol.Parser.AST.TParam instance GHC.Show.Show Cryptol.Parser.AST.Kind instance GHC.Classes.Eq Cryptol.Parser.AST.Kind instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.Named a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.Named a) instance GHC.Classes.Ord Cryptol.Parser.AST.Selector instance GHC.Show.Show Cryptol.Parser.AST.Selector instance GHC.Classes.Eq Cryptol.Parser.AST.Selector instance GHC.Show.Show Cryptol.Parser.AST.Literal instance GHC.Classes.Eq Cryptol.Parser.AST.Literal instance GHC.Show.Show Cryptol.Parser.AST.NumInfo instance GHC.Classes.Eq Cryptol.Parser.AST.NumInfo instance GHC.Show.Show Cryptol.Parser.AST.ExportSpec instance GHC.Classes.Ord a => GHC.Classes.Ord (Cryptol.Parser.AST.TopLevel a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.TopLevel a) instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.TopLevel a) instance GHC.Classes.Ord Cryptol.Parser.AST.ExportType instance GHC.Show.Show Cryptol.Parser.AST.ExportType instance GHC.Classes.Eq Cryptol.Parser.AST.ExportType instance GHC.Show.Show Cryptol.Parser.AST.Pragma instance GHC.Classes.Eq Cryptol.Parser.AST.Pragma instance GHC.Show.Show Cryptol.Parser.AST.Import instance GHC.Classes.Eq Cryptol.Parser.AST.Import instance GHC.Show.Show Cryptol.Parser.AST.ImportSpec instance GHC.Classes.Eq Cryptol.Parser.AST.ImportSpec instance GHC.Show.Show Cryptol.Parser.AST.QName instance GHC.Classes.Ord Cryptol.Parser.AST.QName instance GHC.Classes.Eq Cryptol.Parser.AST.QName instance GHC.Show.Show Cryptol.Parser.AST.Name instance GHC.Classes.Ord Cryptol.Parser.AST.Name instance GHC.Classes.Eq Cryptol.Parser.AST.Name instance GHC.Show.Show Cryptol.Parser.AST.Pass instance GHC.Classes.Ord Cryptol.Parser.AST.Pass instance GHC.Classes.Eq Cryptol.Parser.AST.Pass instance GHC.Show.Show Cryptol.Parser.AST.ModName instance GHC.Classes.Ord Cryptol.Parser.AST.ModName instance GHC.Classes.Eq Cryptol.Parser.AST.ModName instance GHC.Base.Functor Cryptol.Parser.AST.TopLevel instance GHC.Base.Monoid Cryptol.Parser.AST.ExportSpec instance GHC.Base.Functor Cryptol.Parser.AST.Named instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Expr instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Expr instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.TParam instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.TParam instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Type instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Type instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Prop instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Prop instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Pattern instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Pattern instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Bind instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Match instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Named a) instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Schema instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Schema instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Decl instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Decl instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.TopDecl instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Module instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Newtype instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Module instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Program instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TopDecl instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Decl instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Newtype instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Import instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ImportSpec instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pragma instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Bind instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TySyn instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ModName instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.QName instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Name instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Literal instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TypeInst instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Expr instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Selector instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pattern instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Match instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Schema instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Kind instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TParam instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Type instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Prop instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.Position.Located t) instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Named t) instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos [t] instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (GHC.Base.Maybe t) instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Program instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Module instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TopDecl instance Cryptol.Parser.AST.NoPos a => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopLevel a) instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Decl instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Newtype instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Bind instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pragma instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TySyn instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Expr instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TypeInst instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Match instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pattern instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Schema instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TParam instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Type instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Prop 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 GHC.Show.Show Cryptol.TypeCheck.AST.Module instance GHC.Show.Show Cryptol.TypeCheck.AST.Match instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclGroup instance GHC.Show.Show Cryptol.TypeCheck.AST.Expr instance GHC.Show.Show Cryptol.TypeCheck.AST.Decl instance GHC.Show.Show Cryptol.TypeCheck.AST.Schema instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Schema instance GHC.Show.Show Cryptol.TypeCheck.AST.TySyn instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TySyn instance GHC.Show.Show Cryptol.TypeCheck.AST.Newtype instance GHC.Classes.Ord Cryptol.TypeCheck.AST.Type instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Type instance GHC.Show.Show Cryptol.TypeCheck.AST.Type instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TCon instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TCon instance GHC.Show.Show Cryptol.TypeCheck.AST.TCon instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TC instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TC instance GHC.Show.Show Cryptol.TypeCheck.AST.TC instance GHC.Show.Show Cryptol.TypeCheck.AST.UserTC instance GHC.Classes.Ord Cryptol.TypeCheck.AST.PC instance GHC.Classes.Eq Cryptol.TypeCheck.AST.PC instance GHC.Show.Show Cryptol.TypeCheck.AST.PC instance GHC.Show.Show Cryptol.TypeCheck.AST.TVar instance GHC.Show.Show Cryptol.TypeCheck.AST.TParam instance GHC.Show.Show Cryptol.TypeCheck.AST.Kind instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Kind instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TParam instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TParam instance GHC.Classes.Eq Cryptol.TypeCheck.AST.UserTC instance GHC.Classes.Ord Cryptol.TypeCheck.AST.UserTC instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TVar instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TVar instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TVar instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TCon instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.UserTC instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TC instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.PC instance Cryptol.TypeCheck.AST.HasKind Cryptol.Prims.Syntax.TFun instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.Type instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TySyn instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.Newtype instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TParam instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Kind instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TVar) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TParam instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TParam) instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Type) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Schema instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Schema) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TySyn instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TySyn) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Type instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TCon instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.PC instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TC instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.UserTC instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Expr) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Expr instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Match) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Match instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclGroup) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Decl) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Decl instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Module instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Module) 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 GHC.Show.Show Cryptol.Eval.Error.EvalError instance Cryptol.Utils.PP.PP Cryptol.Eval.Error.EvalError instance GHC.Exception.Exception Cryptol.Eval.Error.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 -- | NOTE this assumes that the sequence of bits is big-endian and finite, -- so the first element of the list will be the most significant bit. packWord :: BitWord b w => [b] -> w -- | NOTE this produces a list of bits that represent a big-endian word, so -- the most significant bit is the first element of the list. unpackWord :: BitWord b w => 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 GHC.Base.Functor Cryptol.Eval.Value.WithBase instance GHC.Show.Show Cryptol.Eval.Value.TValue instance Cryptol.Utils.PP.PP (Cryptol.Eval.Value.WithBase Cryptol.Eval.Value.Value) instance Cryptol.Eval.Value.BitWord GHC.Types.Bool Cryptol.Eval.Value.BV -- | 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 SBool = SVal type SWord = SVal literalSWord :: Int -> Integer -> SWord fromBitsLE :: [SBool] -> SWord forallBV_ :: Int -> Symbolic SWord existsBV_ :: Int -> Symbolic SWord forallSBool_ :: Symbolic SBool existsSBool_ :: Symbolic SBool 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 iteValue :: SBool -> Value -> Value -> Value mergeValue :: Bool -> SBool -> Value -> Value -> Value instance Cryptol.Eval.Value.BitWord Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord -- | 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 GHC.Base.Monoid Cryptol.Eval.Env.EvalEnv instance Cryptol.Utils.PP.PP (Cryptol.Eval.Value.WithBase Cryptol.Eval.Env.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 GHC.Base.Functor Cryptol.TypeCheck.TypeMap.TypeMap instance GHC.Base.Functor m => GHC.Base.Functor (Cryptol.TypeCheck.TypeMap.List m) instance Cryptol.TypeCheck.TypeMap.TrieMap m a => Cryptol.TypeCheck.TypeMap.TrieMap (Cryptol.TypeCheck.TypeMap.List m) [a] instance GHC.Classes.Ord a => Cryptol.TypeCheck.TypeMap.TrieMap (Data.Map.Base.Map a) a instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.TypeCheck.TypeMap.TypeMap Cryptol.TypeCheck.AST.Type instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.TypeMap.TypeMap 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 GHC.Show.Show Cryptol.TypeCheck.Subst.Subst instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Subst.Subst) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Subst.Subst instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.AST.Type instance Cryptol.TypeCheck.Subst.FVS a => Cryptol.TypeCheck.Subst.FVS [a] instance (Cryptol.TypeCheck.Subst.FVS a, Cryptol.TypeCheck.Subst.FVS b) => Cryptol.TypeCheck.Subst.FVS (a, b) instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.AST.Schema instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars (GHC.Base.Maybe t) instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars [t] instance (Cryptol.TypeCheck.Subst.TVars s, Cryptol.TypeCheck.Subst.TVars t) => Cryptol.TypeCheck.Subst.TVars (s, t) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Type instance (GHC.Base.Functor m, Cryptol.TypeCheck.Subst.TVars a) => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.List m a) instance Cryptol.TypeCheck.Subst.TVars a => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.TypeMap a) instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Schema instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Expr instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Match instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclGroup instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Decl instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module 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 GHC.Base.Functor Cryptol.TypeCheck.Unify.Result instance GHC.Base.Applicative Cryptol.TypeCheck.Unify.Result instance GHC.Base.Monad Cryptol.TypeCheck.Unify.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 GHC.Show.Show Cryptol.ModuleSystem.Interface.Iface instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecls instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecl instance GHC.Base.Monoid Cryptol.ModuleSystem.Interface.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 Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.Transform.MonoValues.RewMap' (Cryptol.Parser.AST.QName, [Cryptol.TypeCheck.AST.Type], GHC.Types.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 GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NamingEnv instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.TName instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.EName instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NameOrigin instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.NamingEnv.NameOrigin instance Cryptol.ModuleSystem.NamingEnv.HasQName Cryptol.ModuleSystem.NamingEnv.TName instance Cryptol.ModuleSystem.NamingEnv.HasQName Cryptol.ModuleSystem.NamingEnv.EName instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.NamingEnv instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.NamingEnv instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames (GHC.Base.Maybe a) instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames [a] instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Schema instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.Interface.Iface instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.Interface.IfaceDecls instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Match instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Bind instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.TParam instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Pattern instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Module instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Decl -- | The purpose of this module is to convert all patterns to variable -- patterns. It also eliminates pattern bindings by de-sugaring them into -- Bind. Furthermore, here we associate signatures and pragmas -- with the names to which they belong. module Cryptol.Parser.NoPat class RemovePatterns t -- | Eliminate all patterns in a program. removePatterns :: RemovePatterns t => t -> (t, [Error]) data Error MultipleSignatures :: QName -> [Located Schema] -> Error SignatureNoBind :: (Located QName) -> Schema -> Error PragmaNoBind :: (Located QName) -> Pragma -> Error instance GHC.Show.Show Cryptol.Parser.NoPat.Error instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Program instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Expr instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Module instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl] instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error -- | 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 GHC.Show.Show Cryptol.Parser.NoInclude.IncludeError instance GHC.Base.Functor Cryptol.Parser.NoInclude.NoIncM instance GHC.Base.Applicative Cryptol.Parser.NoInclude.NoIncM instance GHC.Base.Monad Cryptol.Parser.NoInclude.NoIncM module Cryptol.ModuleSystem.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 GHC.Show.Show Cryptol.ModuleSystem.Renamer.Out instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerWarning instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerError instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerError instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerWarning instance GHC.Base.Monoid Cryptol.ModuleSystem.Renamer.Out instance GHC.Base.Functor Cryptol.ModuleSystem.Renamer.RenameM instance GHC.Base.Applicative Cryptol.ModuleSystem.Renamer.RenameM instance GHC.Base.Monad Cryptol.ModuleSystem.Renamer.RenameM instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename [a] instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (GHC.Base.Maybe a) instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.Position.Located a) instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.AST.Named a) instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Module instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TopDecl instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.AST.TopLevel a) instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Decl instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Newtype instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Schema instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Prop instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Type instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pragma instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Bind instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pattern instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Expr instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TypeInst instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Match instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TySyn -- | 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 GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goals instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.HasGoal instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Error instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.DelayedCt instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Solved instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goal instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.ConstraintSource instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.TyFunName instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Warning instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.TyFunName instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.ConstraintSource instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Warning instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Warning instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Error instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Error instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.DelayedCt instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goals instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.HasGoal instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.DelayedCt instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Warning instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Error instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Warning) instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Error) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.ConstraintSource instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Goal) instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.DelayedCt) instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Solved 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 GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.Monad.InferOutput a) instance GHC.Show.Show Cryptol.TypeCheck.Monad.InferInput instance GHC.Show.Show Cryptol.TypeCheck.Monad.NameSeeds instance GHC.Base.Functor Cryptol.TypeCheck.Monad.InferM instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.InferM instance GHC.Base.Monad Cryptol.TypeCheck.Monad.InferM instance Control.Monad.Fix.MonadFix Cryptol.TypeCheck.Monad.InferM instance GHC.Base.Functor Cryptol.TypeCheck.Monad.KindM instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.KindM instance GHC.Base.Monad Cryptol.TypeCheck.Monad.KindM 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 Cryptol.TypeCheck.Depends.FromDecl Cryptol.Parser.AST.TopDecl instance Cryptol.TypeCheck.Depends.FromDecl Cryptol.Parser.AST.Decl 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 GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.AssertResult instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.OrdFacts instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Edges instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Edge instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.NumType instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.NumType instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.NumType instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Nat'' instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.Nat'' instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.Nat'' instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.EdgeSrc instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.OrdTerms instance Cryptol.TypeCheck.Solver.FinOrd.IsFact Cryptol.TypeCheck.InferTypes.Goal instance Cryptol.TypeCheck.Solver.FinOrd.IsFact Cryptol.TypeCheck.AST.Prop instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.Edge instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.Edge -- | 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 GHC.Show.Show Cryptol.TypeCheck.Solver.Smtlib.SMTResult instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Smtlib.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 GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModules instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModule instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.LoadedModules instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.DynamicEnv 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 GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleWarning instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleError instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ImportSource instance GHC.Classes.Eq Cryptol.ModuleSystem.Monad.ImportSource instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ImportSource instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleError instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleWarning instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Monad.ModuleT m) instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Monad.ModuleT m) instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Monad.ModuleT m) instance MonadLib.MonadT Cryptol.ModuleSystem.Monad.ModuleT 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 -> TValue -> 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 :: SWord -> SWord -> SBool -> SBool cmpNotEq :: SWord -> SWord -> SBool -> SBool cmpLt :: SWord -> SWord -> SBool -> SBool cmpGt :: SWord -> SWord -> SBool -> SBool cmpLtEq :: SWord -> SWord -> SBool -> SBool cmpGtEq :: SWord -> SWord -> 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 smtMode :: Bool 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) -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult satProveOffline :: Bool -> Bool -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult protectStack :: 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 -> Env [envVars] :: Env -> Map QName Value [envTypes] :: Env -> Map TVar TValue emptyEnv :: 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 GHC.Base.Monoid Cryptol.Symbolic.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 GHC.Classes.Eq Cryptol.REPL.Monad.Smoke instance GHC.Show.Show Cryptol.REPL.Monad.Smoke instance GHC.Show.Show Cryptol.REPL.Monad.EnvVal instance GHC.Show.Show Cryptol.REPL.Monad.REPLException instance GHC.Base.Functor Cryptol.REPL.Monad.REPL instance GHC.Base.Applicative Cryptol.REPL.Monad.REPL instance GHC.Base.Monad Cryptol.REPL.Monad.REPL instance GHC.Exception.Exception Cryptol.REPL.Monad.REPLException instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.REPLException instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.Smoke 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 GHC.Show.Show Cryptol.REPL.Command.QCMode instance GHC.Classes.Eq Cryptol.REPL.Command.QCMode instance GHC.Show.Show Cryptol.REPL.Command.CommandDescr instance GHC.Classes.Eq Cryptol.REPL.Command.CommandDescr instance GHC.Classes.Ord Cryptol.REPL.Command.CommandDescr