-- 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.8.0

-- | Architecture-specific parts of the concrete evaluator go here.
module Cryptol.Eval.Arch

-- | This is the widest word we can have before gmp will fail to allocate
--   and bring down the whole program. According to
--   https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html
--   the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however
--   experiments show that it's somewhere under 2^37 at least on 64-bit Mac
--   OS X.
maxBigIntWidth :: Integer

module Cryptol.ModuleSystem.Fingerprint
data Fingerprint

-- | Compute a fingerprint for a bytestring.
fingerprint :: ByteString -> Fingerprint

-- | Attempt to compute the fingerprint of the file at the given path.
--   Returns Nothing in the case of an error.
fingerprintFile :: FilePath -> IO (Maybe Fingerprint)
instance GHC.Show.Show Cryptol.ModuleSystem.Fingerprint.Fingerprint
instance GHC.Classes.Eq Cryptol.ModuleSystem.Fingerprint.Fingerprint
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Fingerprint.Fingerprint

module Cryptol.Utils.Ident

-- | Module names are just text.
data ModName
modNameToText :: ModName -> Text
textToModName :: Text -> ModName
modNameChunks :: ModName -> [String]
packModName :: [Text] -> ModName
preludeName :: ModName
interactiveName :: ModName
noModuleName :: ModName
exprModName :: ModName
isParamInstModName :: ModName -> Bool

-- | Convert a parameterized module's name to the name of the module
--   containing the same definitions but with explicit parameters on each
--   definition.
paramInstModName :: ModName -> ModName
notParamInstModName :: ModName -> ModName

-- | Identifiers, along with a flag that indicates whether or not they're
--   infix operators. The boolean is present just as cached information
--   from the lexer, and never used during comparisons.
data Ident
packIdent :: String -> Ident
packInfix :: String -> Ident
unpackIdent :: Ident -> String
mkIdent :: Text -> Ident
mkInfix :: Text -> Ident
isInfixIdent :: Ident -> Bool
nullIdent :: Ident -> Bool
identText :: Ident -> Text
modParamIdent :: Ident -> Ident
instance GHC.Generics.Generic Cryptol.Utils.Ident.Ident
instance GHC.Show.Show Cryptol.Utils.Ident.Ident
instance GHC.Generics.Generic Cryptol.Utils.Ident.ModName
instance GHC.Show.Show Cryptol.Utils.Ident.ModName
instance GHC.Classes.Ord Cryptol.Utils.Ident.ModName
instance GHC.Classes.Eq Cryptol.Utils.Ident.ModName
instance GHC.Classes.Eq Cryptol.Utils.Ident.Ident
instance GHC.Classes.Ord Cryptol.Utils.Ident.Ident
instance Data.String.IsString Cryptol.Utils.Ident.Ident
instance Control.DeepSeq.NFData Cryptol.Utils.Ident.Ident
instance Control.DeepSeq.NFData Cryptol.Utils.Ident.ModName

-- | A simple system so that the Cryptol driver can communicate with users
--   (or not).
module Cryptol.Utils.Logger

-- | A logger provides simple abstraction for sending messages.
data Logger

-- | Log to stdout.
stdoutLogger :: Logger

-- | Log to stderr.
stderrLogger :: Logger

-- | Log to the given handle.
handleLogger :: Handle -> Logger

-- | A logger that ignores all messages.
quietLogger :: Logger

-- | Just use this function for logging.
funLogger :: (String -> IO ()) -> Logger

-- | Send the given string to the log.
logPutStr :: Logger -> String -> IO ()

-- | Send the given string with a newline at the end.
logPutStrLn :: Logger -> String -> IO ()

-- | Send the given value using its Show instance. Adds a newline at
--   the end.
logPrint :: Show a => Logger -> a -> IO ()
instance Control.DeepSeq.NFData Cryptol.Utils.Logger.Logger

module Cryptol.Utils.Misc

-- | Apply a function to all elements of a container. Returns
--   Nothing if nothing changed, and Just container
--   otherwise.
anyJust :: Traversable t => (a -> Maybe a) -> t a -> Maybe (t a)

-- | Apply functions to both elements of a pair. Returns Nothing if
--   neither changed, and Just pair otherwise.
anyJust2 :: (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)

module Cryptol.Utils.PP

-- | How to display names, inspired by the GHC Outputable module.
--   Getting a value of Nothing from the NameDisp function indicates
--   that the display has no opinion on how this name should be displayed,
--   and some other display should be tried out.
data NameDisp
EmptyNameDisp :: NameDisp
NameDisp :: (ModName -> Ident -> Maybe NameFormat) -> NameDisp
data NameFormat
UnQualified :: NameFormat
Qualified :: !ModName -> NameFormat
NotInScope :: NameFormat

-- | Never qualify names from this module.
neverQualifyMod :: ModName -> NameDisp
alwaysQualify :: NameDisp
neverQualify :: NameDisp
fmtModName :: ModName -> NameFormat -> Text

-- | Compose two naming environments, preferring names from the left
--   environment.
extend :: NameDisp -> NameDisp -> NameDisp

-- | Get the format for a name. When Nothing is returned, the name
--   is not currently in scope.
getNameFormat :: ModName -> Ident -> NameDisp -> NameFormat

-- | Produce a document in the context of the current NameDisp.
withNameDisp :: (NameDisp -> Doc) -> Doc

-- | Fix the way that names are displayed inside of a doc.
fixNameDisp :: NameDisp -> Doc -> Doc
newtype Doc
Doc :: (NameDisp -> Doc) -> Doc
runDoc :: NameDisp -> Doc -> Doc
render :: Doc -> String
renderOneLine :: Doc -> String
class PP a
ppPrec :: PP a => Int -> a -> Doc
class PP a => PPName a

-- | Fixity information for infix operators
ppNameFixity :: PPName a => a -> Maybe (Assoc, Int)

-- | Print a name in prefix: f a b or (+) a b)
ppPrefixName :: PPName a => a -> Doc

-- | Print a name as an infix operator: a + b
ppInfixName :: PPName a => a -> Doc
pp :: PP a => a -> Doc
pretty :: PP a => a -> String
optParens :: Bool -> Doc -> Doc

-- | Information about associativity.
data Assoc
LeftAssoc :: Assoc
RightAssoc :: Assoc
NonAssoc :: Assoc

-- | Information about an infix expression of some sort.
data Infix op thing
Infix :: op -> thing -> thing -> Int -> Assoc -> Infix op thing

-- | operator
[ieOp] :: Infix op thing -> op

-- | left argument
[ieLeft] :: Infix op thing -> thing

-- | right argument
[ieRight] :: Infix op thing -> thing

-- | operator precedence
[iePrec] :: Infix op thing -> Int

-- | operator associativity
[ieAssoc] :: Infix op thing -> Assoc
commaSep :: [Doc] -> Doc

-- | Pretty print an infix expression of some sort.
ppInfix :: (PP thing, PP op) => Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc

-- | Display a numeric value as an ordinal (e.g., 2nd)
ordinal :: (Integral a, Show a, Eq a) => a -> Doc

-- | The suffix to use when displaying a number as an oridinal
ordSuffix :: (Integral a, Eq a) => a -> String
liftPJ :: Doc -> Doc
liftPJ1 :: (Doc -> Doc) -> Doc -> Doc
liftPJ2 :: (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc
liftSep :: ([Doc] -> Doc) -> [Doc] -> Doc
(<.>) :: Doc -> Doc -> Doc
infixl 6 <.>
(<+>) :: Doc -> Doc -> Doc
infixl 6 <+>
($$) :: Doc -> Doc -> Doc
infixl 5 $$
sep :: [Doc] -> Doc
fsep :: [Doc] -> Doc
hsep :: [Doc] -> Doc
hcat :: [Doc] -> Doc
vcat :: [Doc] -> Doc
hang :: Doc -> Int -> Doc -> Doc
nest :: Int -> Doc -> Doc
parens :: Doc -> Doc
braces :: Doc -> Doc
brackets :: Doc -> Doc
quotes :: Doc -> Doc
backticks :: Doc -> Doc
punctuate :: Doc -> [Doc] -> [Doc]
text :: String -> Doc
char :: Char -> Doc
integer :: Integer -> Doc
int :: Int -> Doc
comma :: Doc
empty :: Doc
colon :: Doc
instance Control.DeepSeq.NFData Cryptol.Utils.PP.Assoc
instance GHC.Generics.Generic Cryptol.Utils.PP.Assoc
instance GHC.Classes.Eq Cryptol.Utils.PP.Assoc
instance GHC.Show.Show Cryptol.Utils.PP.Assoc
instance Control.DeepSeq.NFData Cryptol.Utils.PP.Doc
instance GHC.Generics.Generic Cryptol.Utils.PP.Doc
instance Control.DeepSeq.NFData Cryptol.Utils.PP.NameDisp
instance GHC.Generics.Generic Cryptol.Utils.PP.NameDisp
instance GHC.Show.Show Cryptol.Utils.PP.NameFormat
instance Cryptol.Utils.PP.PP Cryptol.Utils.PP.Assoc
instance Cryptol.Utils.PP.PP Data.Text.Internal.Text
instance Cryptol.Utils.PP.PP Cryptol.Utils.Ident.Ident
instance Cryptol.Utils.PP.PP Cryptol.Utils.Ident.ModName
instance GHC.Base.Semigroup Cryptol.Utils.PP.Doc
instance GHC.Base.Monoid Cryptol.Utils.PP.Doc
instance GHC.Show.Show Cryptol.Utils.PP.Doc
instance Data.String.IsString Cryptol.Utils.PP.Doc
instance GHC.Show.Show Cryptol.Utils.PP.NameDisp
instance GHC.Base.Semigroup Cryptol.Utils.PP.NameDisp
instance GHC.Base.Monoid Cryptol.Utils.PP.NameDisp

module Cryptol.Utils.Debug
trace :: String -> b -> b
ppTrace :: Doc -> b -> b

module Cryptol.TypeCheck.PP
type NameMap = IntMap String

-- | This packages together a type with some names to be used to display
--   the variables. It is used for pretty printing types.
data WithNames a
WithNames :: a -> NameMap -> WithNames a
emptyNameMap :: NameMap
ppWithNamesPrec :: PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNames :: PP (WithNames a) => NameMap -> a -> Doc

-- | Expand a list of base names into an infinite list of variations.
nameList :: [String] -> [String]
dump :: PP (WithNames a) => a -> String

module Cryptol.Parser.Selector

-- | Selectors are used for projecting from various components. Each
--   selector has an option spec to specify the shape of the thing that is
--   being selected. Currently, there is no surface syntax for list
--   selectors, but they are used during the desugaring of patterns.
data Selector

-- | Zero-based tuple selection. Optionally specifies the shape of the
--   tuple (one-based).
TupleSel :: Int -> Maybe Int -> Selector

-- | Record selection. Optionally specifies the shape of the record.
RecordSel :: Ident -> Maybe [Ident] -> Selector

-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> Maybe Int -> Selector

-- | Display the thing selected by the selector, nicely.
ppSelector :: Selector -> Doc

-- | Show a list of selectors as they appear in a nested selector in an
--   update.
ppNestedSels :: [Selector] -> Doc

-- | The name of a selector (e.g., used in update code)
selName :: Selector -> Ident
instance Control.DeepSeq.NFData Cryptol.Parser.Selector.Selector
instance GHC.Generics.Generic Cryptol.Parser.Selector.Selector
instance GHC.Classes.Ord Cryptol.Parser.Selector.Selector
instance GHC.Show.Show Cryptol.Parser.Selector.Selector
instance GHC.Classes.Eq Cryptol.Parser.Selector.Selector
instance Cryptol.Utils.PP.PP Cryptol.Parser.Selector.Selector

module Cryptol.Parser.Position
data Located a
Located :: !Range -> !a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> !a
data Position
Position :: !Int -> !Int -> Position
[line] :: Position -> !Int
[col] :: Position -> !Int
data Range
Range :: !Position -> !Position -> FilePath -> Range
[from] :: Range -> !Position
[to] :: Range -> !Position
[source] :: Range -> FilePath

-- | An empty range.
--   
--   Caution: using this on the LHS of a use of rComb will cause the empty
--   source to propagate.
emptyRange :: Range
start :: Position
move :: Position -> Char -> Position
moves :: Position -> Text -> Position
rComb :: Range -> Range -> Range
rCombs :: [Range] -> Range
class HasLoc t
getLoc :: HasLoc t => t -> Maybe Range
class HasLoc t => AddLoc t
addLoc :: AddLoc t => t -> Range -> t
dropLoc :: AddLoc t => t -> t
at :: (HasLoc l, AddLoc t) => l -> t -> t
combLoc :: (a -> b -> c) -> Located a -> Located b -> Located c
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.Position.Located a)
instance GHC.Generics.Generic (Cryptol.Parser.Position.Located a)
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.Position.Located a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.Position.Located a)
instance Control.DeepSeq.NFData Cryptol.Parser.Position.Range
instance GHC.Generics.Generic Cryptol.Parser.Position.Range
instance GHC.Show.Show Cryptol.Parser.Position.Range
instance GHC.Classes.Eq Cryptol.Parser.Position.Range
instance Control.DeepSeq.NFData Cryptol.Parser.Position.Position
instance GHC.Generics.Generic Cryptol.Parser.Position.Position
instance GHC.Show.Show Cryptol.Parser.Position.Position
instance GHC.Classes.Ord Cryptol.Parser.Position.Position
instance GHC.Classes.Eq Cryptol.Parser.Position.Position
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.Position.Located a)
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.Position.Range
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.Position.Located a)
instance (Cryptol.Parser.Position.HasLoc a, Cryptol.Parser.Position.HasLoc b) => Cryptol.Parser.Position.HasLoc (a, b)
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc [a]
instance GHC.Base.Functor Cryptol.Parser.Position.Located
instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.Position.Located a)
instance Cryptol.Utils.PP.PPName a => Cryptol.Utils.PP.PPName (Cryptol.Parser.Position.Located a)
instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Range
instance Cryptol.Utils.PP.PP Cryptol.Parser.Position.Position

module Cryptol.Parser.Fixity
data Fixity
Fixity :: !Assoc -> !Int -> Fixity
[fAssoc] :: Fixity -> !Assoc
[fLevel] :: Fixity -> !Int

-- | The fixity used when none is provided.
defaultFixity :: Fixity
data FixityCmp
FCError :: FixityCmp
FCLeft :: FixityCmp
FCRight :: FixityCmp
compareFixity :: Fixity -> Fixity -> FixityCmp
instance GHC.Classes.Eq Cryptol.Parser.Fixity.FixityCmp
instance GHC.Show.Show Cryptol.Parser.Fixity.FixityCmp
instance GHC.Show.Show Cryptol.Parser.Fixity.Fixity
instance Control.DeepSeq.NFData Cryptol.Parser.Fixity.Fixity
instance GHC.Generics.Generic Cryptol.Parser.Fixity.Fixity
instance GHC.Classes.Eq Cryptol.Parser.Fixity.Fixity
instance Cryptol.Utils.PP.PP Cryptol.Parser.Fixity.Fixity

module Cryptol.Utils.Panic

-- | Request a CallStack.
--   
--   NOTE: The implicit parameter ?callStack :: CallStack is an
--   implementation detail and should not be considered part of the
--   CallStack API, we may decide to change the implementation in
--   the future.
type HasCallStack = ?callStack :: CallStack
type CryptolPanic = Panic Cryptol
data Cryptol

-- | The exception thrown when panicing.
data Panic a
panic :: HasCallStack => String -> [String] -> a
instance Panic.PanicComponent Cryptol.Utils.Panic.Cryptol

-- | This module defines natural numbers with an additional infinity
--   element, and various arithmetic operators on them.
module Cryptol.TypeCheck.Solver.InfNat

-- | Natural numbers with an infinity element
data Nat'
Nat :: Integer -> Nat'
Inf :: Nat'
fromNat :: Nat' -> Maybe Integer
nAdd :: Nat' -> Nat' -> Nat'

-- | Some algebraic properties of interest:
--   
--   
--   1 * x = x
--   x * (y * z) = (x * y) * z
--   0 * x = 0
--   x * y = y * x
--   x * (a + b) = x * a + x * b
--   
nMul :: Nat' -> Nat' -> Nat'

-- | Some algebraic properties of interest:
--   
--   
--   x ^ 0        = 1
--   x ^ (n + 1)  = x * (x ^ n)
--   x ^ (m + n)  = (x ^ m) * (x ^ n)
--   x ^ (m * n)  = (x ^ m) ^ n
--   
nExp :: Nat' -> Nat' -> Nat'
nMin :: Nat' -> Nat' -> Nat'
nMax :: Nat' -> Nat' -> Nat'

-- | nSub x y = Just z iff z is the unique value such
--   that Add y z = Just x.
nSub :: Nat' -> Nat' -> Maybe Nat'

-- | Rounds down.
--   
--   
--   y * q + r = x
--   x / y     = q with remainder r
--   0 <= r && r < y
--   
--   
--   We don't allow Inf in the first argument for two reasons: 1. It
--   matches the behavior of nMod, 2. The well-formedness
--   constraints can be expressed as a conjunction.
nDiv :: Nat' -> Nat' -> Maybe Nat'
nMod :: Nat' -> Nat' -> Maybe Nat'

-- | nCeilDiv msgLen blockSize computes the least n such
--   that msgLen <= blockSize * n. It is undefined when
--   blockSize = 0. It is also undefined when either input is
--   infinite; perhaps this could be relaxed later.
nCeilDiv :: Nat' -> Nat' -> Maybe Nat'

-- | nCeilMod msgLen blockSize computes the least k such
--   that blockSize divides msgLen + k. It is undefined
--   when blockSize = 0. It is also undefined when either input is
--   infinite; perhaps this could be relaxed later.
nCeilMod :: Nat' -> Nat' -> Maybe Nat'

-- | Rounds up. lg2 x = y, iff y is the smallest number
--   such that x <= 2 ^ y
nLg2 :: Nat' -> Nat'

-- | nWidth n is number of bits needed to represent all numbers
--   from 0 to n, inclusive. nWidth x = nLg2 (x + 1).
nWidth :: Nat' -> Nat'

-- | 
--   length [ x, y .. z ]
--   
nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'

-- | Compute the logarithm of a number in the given base, rounded down to
--   the closest integer. The boolean indicates if we the result is exact
--   (i.e., True means no rounding happened, False means we rounded down).
--   The logarithm base is the second argument.
genLog :: Integer -> Integer -> Maybe (Integer, Bool)

-- | Compute the number of bits required to represent the given integer.
widthInteger :: Integer -> Integer

-- | Compute the exact root of a natural number. The second argument
--   specifies which root we are computing.
rootExact :: Integer -> Integer -> Maybe Integer

-- | Compute the the n-th root of a natural number, rounded down to the
--   closest natural number. The boolean indicates if the result is exact
--   (i.e., True means no rounding was done, False means rounded down). The
--   second argument specifies which root we are computing.
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Show.Show Cryptol.TypeCheck.Solver.InfNat.Nat'

module Cryptol.REPL.Trie

-- | Maps string names to values, allowing for partial key matches and
--   querying.
data Trie a
Node :: Map Char (Trie a) -> Maybe a -> Trie a
emptyTrie :: Trie a

-- | Insert a value into the Trie. Will call panic if a value
--   already exists with that key.
insertTrie :: String -> a -> Trie a -> Trie a

-- | Return all matches with the given prefix.
lookupTrie :: String -> Trie a -> [a]

-- | Given a key, return either an exact match for that key, or all matches
--   with the given prefix.
lookupTrieExact :: String -> Trie a -> [a]

-- | Return all of the values from a Trie.
leaves :: Trie a -> [a]
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.REPL.Trie.Trie a)

-- | Convert a literate source file into an ordinary source file.
module Cryptol.Parser.Unlit
unLit :: PreProc -> Text -> Text
data PreProc
None :: PreProc
Markdown :: PreProc
LaTeX :: PreProc
guessPreProc :: FilePath -> PreProc
knownExts :: [String]

module Cryptol.Parser.Name

-- | Names that originate in the parser.
data PName

-- | Unqualified names like x, Foo, or +.
UnQual :: !Ident -> PName

-- | Qualified names like Foo::bar or module::!.
Qual :: !ModName -> !Ident -> PName

-- | Fresh names generated by a pass.
NewName :: !Pass -> !Int -> PName

-- | Passes that can generate fresh names.
data Pass
NoPat :: Pass
MonoValues :: Pass
mkUnqual :: Ident -> PName
mkQual :: ModName -> Ident -> PName
getModName :: PName -> Maybe ModName
getIdent :: PName -> Ident
isGeneratedName :: PName -> Bool
instance GHC.Generics.Generic Cryptol.Parser.Name.PName
instance GHC.Show.Show Cryptol.Parser.Name.PName
instance GHC.Classes.Ord Cryptol.Parser.Name.PName
instance GHC.Classes.Eq Cryptol.Parser.Name.PName
instance GHC.Generics.Generic Cryptol.Parser.Name.Pass
instance GHC.Show.Show Cryptol.Parser.Name.Pass
instance GHC.Classes.Ord Cryptol.Parser.Name.Pass
instance GHC.Classes.Eq Cryptol.Parser.Name.Pass
instance Control.DeepSeq.NFData Cryptol.Parser.Name.PName
instance Cryptol.Utils.PP.PP Cryptol.Parser.Name.PName
instance Cryptol.Utils.PP.PPName Cryptol.Parser.Name.PName
instance Control.DeepSeq.NFData Cryptol.Parser.Name.Pass

module Cryptol.Parser.AST

-- | Identifiers, along with a flag that indicates whether or not they're
--   infix operators. The boolean is present just as cached information
--   from the lexer, and never used during comparisons.
data Ident
mkIdent :: Text -> Ident
mkInfix :: Text -> Ident
isInfixIdent :: Ident -> Bool
nullIdent :: Ident -> Bool
identText :: Ident -> Text

-- | Module names are just text.
data ModName
modRange :: Module name -> Range

-- | Names that originate in the parser.
data PName

-- | Unqualified names like x, Foo, or +.
UnQual :: !Ident -> PName

-- | Qualified names like Foo::bar or module::!.
Qual :: !ModName -> !Ident -> PName

-- | Fresh names generated by a pass.
NewName :: !Pass -> !Int -> PName
getModName :: PName -> Maybe ModName
getIdent :: PName -> Ident
mkUnqual :: Ident -> PName
mkQual :: ModName -> Ident -> PName
data Named a
Named :: Located Ident -> a -> Named a
[name] :: Named a -> Located Ident
[value] :: Named a -> a

-- | Passes that can generate fresh names.
data Pass
NoPat :: Pass
MonoValues :: Pass

-- | Information about associativity.
data Assoc
LeftAssoc :: Assoc
RightAssoc :: Assoc
NonAssoc :: Assoc
data Schema n
Forall :: [TParam n] -> [Prop n] -> Type n -> Maybe Range -> Schema n
data TParam n
TParam :: n -> Maybe Kind -> Maybe Range -> TParam n
[tpName] :: TParam n -> n
[tpKind] :: TParam n -> Maybe Kind
[tpRange] :: TParam n -> Maybe Range
data Kind
KProp :: Kind
KNum :: Kind
KType :: Kind
KFun :: Kind -> Kind -> Kind
data Type n

-- | 
--   [8] -> [8]
--   
TFun :: Type n -> Type n -> Type n

-- | 
--   [8] a
--   
TSeq :: Type n -> Type n -> Type n

-- | 
--   Bit
--   
TBit :: Type n

-- | 
--   10
--   
TNum :: Integer -> Type n

-- | 
--   a
--   
TChar :: Char -> Type n

-- | A type variable or synonym
TUser :: n -> [Type n] -> Type n

-- | 
--   { x : [8], y : [32] }
--   
TRecord :: [Named (Type n)] -> Type n

-- | 
--   ([8], [32])
--   
TTuple :: [Type n] -> Type n

-- | _, just some type.
TWild :: Type n

-- | Location information
TLocated :: Type n -> Range -> Type n

-- | 
--   (ty)
--   
TParens :: Type n -> Type n

-- | 
--   ty + ty
--   
TInfix :: Type n -> Located n -> Fixity -> Type n -> Type n

-- | A Prop is a Type that represents a type constraint.
newtype Prop n
CType :: Type n -> Prop n
tsName :: TySyn name -> Located name
psName :: PropSyn name -> Located name
tsFixity :: TySyn name -> Maybe Fixity
psFixity :: PropSyn name -> Maybe Fixity

-- | A parsed module.
data Module name
Module :: Located ModName -> !Maybe (Located ModName) -> [Located Import] -> [TopDecl name] -> Module name

-- | Name of the module
[mName] :: Module name -> Located ModName

-- | Functor to instantiate (if this is a functor instnaces)
[mInstance] :: Module name -> !Maybe (Located ModName)

-- | Imports for the module
[mImports] :: Module name -> [Located Import]

-- | Declartions for the module
[mDecls] :: Module name -> [TopDecl name]
newtype Program name
Program :: [TopDecl name] -> Program name
data TopDecl name
Decl :: TopLevel (Decl name) -> TopDecl name
DPrimType :: TopLevel (PrimType name) -> TopDecl name

-- | @newtype T as = t
TDNewtype :: TopLevel (Newtype name) -> TopDecl name

-- | 
--   include File
--   
Include :: Located FilePath -> TopDecl name

-- | 
--   parameter type T : #
--   
DParameterType :: ParameterType name -> TopDecl name

-- | 
--   parameter type constraint (fin T)
--   
DParameterConstraint :: [Located (Prop name)] -> TopDecl name

-- | 
--   parameter someVal : [256]
--   
DParameterFun :: ParameterFun name -> TopDecl name
data Decl name
DSignature :: [Located name] -> Schema name -> Decl name
DFixity :: !Fixity -> [Located name] -> Decl name
DPragma :: [Located name] -> Pragma -> Decl name
DBind :: Bind name -> Decl name
DPatBind :: Pattern name -> Expr name -> Decl name
DType :: TySyn name -> Decl name
DProp :: PropSyn name -> Decl name
DLocated :: Decl name -> Range -> Decl name
data Fixity
Fixity :: !Assoc -> !Int -> Fixity
[fAssoc] :: Fixity -> !Assoc
[fLevel] :: Fixity -> !Int

-- | The fixity used when none is provided.
defaultFixity :: Fixity
data FixityCmp
FCError :: FixityCmp
FCLeft :: FixityCmp
FCRight :: FixityCmp
compareFixity :: Fixity -> Fixity -> FixityCmp
data TySyn n
TySyn :: Located n -> Maybe Fixity -> [TParam n] -> Type n -> TySyn n
data PropSyn n
PropSyn :: Located n -> Maybe Fixity -> [TParam n] -> [Prop n] -> PropSyn n

-- | Bindings. Notes:
--   
--   
--   
- The parser does not associate type signatures and pragmas with
--   their bindings: this is done in a separate pass, after de-sugaring
--   pattern bindings. In this way we can associate pragmas and type
--   signatures with the variables defined by pattern bindings as
--   well.
--   
- Currently, there is no surface syntax for defining monomorphic
--   bindings (i.e., bindings that will not be automatically generalized by
--   the type checker. However, they are useful when de-sugaring
--   patterns.
--   
data Bind name
Bind :: Located name -> [Pattern name] -> Located (BindDef name) -> Maybe (Schema name) -> Bool -> Maybe Fixity -> [Pragma] -> Bool -> Maybe String -> Bind name

-- | Defined thing
[bName] :: Bind name -> Located name

-- | Parameters
[bParams] :: Bind name -> [Pattern name]

-- | Definition
[bDef] :: Bind name -> Located (BindDef name)

-- | Optional type sig
[bSignature] :: Bind name -> Maybe (Schema name)

-- | Infix operator?
[bInfix] :: Bind name -> Bool

-- | Optional fixity info
[bFixity] :: Bind name -> Maybe Fixity

-- | Optional pragmas
[bPragmas] :: Bind name -> [Pragma]

-- | Is this a monomorphic binding
[bMono] :: Bind name -> Bool

-- | Optional doc string
[bDoc] :: Bind name -> Maybe String
data BindDef name
DPrim :: BindDef name
DExpr :: Expr name -> BindDef name
type LBindDef = Located (BindDef PName)
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma

-- | Export information for a declaration.
data ExportType
Public :: ExportType
Private :: ExportType

-- | A top-level module declaration.
data TopLevel a
TopLevel :: ExportType -> Maybe (Located String) -> a -> TopLevel a
[tlExport] :: TopLevel a -> ExportType
[tlDoc] :: TopLevel a -> Maybe (Located String)
[tlValue] :: TopLevel a -> a

-- | An import declaration.
data Import
Import :: !ModName -> Maybe ModName -> Maybe ImportSpec -> Import
[iModule] :: Import -> !ModName
[iAs] :: Import -> Maybe ModName
[iSpec] :: Import -> Maybe ImportSpec

-- | The list of names following an import.
--   
--   INVARIANT: All of the Name entries in the list are expected
--   to be unqualified names; the QName or NewName
--   constructors should not be present.
data ImportSpec
Hiding :: [Ident] -> ImportSpec
Only :: [Ident] -> ImportSpec
data Newtype name
Newtype :: Located name -> [TParam name] -> [Named (Type name)] -> Newtype name

-- | Type name
[nName] :: Newtype name -> Located name

-- | Type params
[nParams] :: Newtype name -> [TParam name]

-- | Constructor
[nBody] :: Newtype name -> [Named (Type name)]

-- | A declaration for a type with no implementation.
data PrimType name
PrimType :: Located name -> Located Kind -> ([TParam name], [Prop name]) -> Maybe Fixity -> PrimType name
[primTName] :: PrimType name -> Located name
[primTKind] :: PrimType name -> Located Kind

-- | parameters are in the order used by the type constructor.
[primTCts] :: PrimType name -> ([TParam name], [Prop name])
[primTFixity] :: PrimType name -> Maybe Fixity

-- | A type parameter
data ParameterType name
ParameterType :: Located name -> Kind -> Maybe String -> Maybe Fixity -> !Int -> ParameterType name

-- | name of type parameter
[ptName] :: ParameterType name -> Located name

-- | kind of parameter
[ptKind] :: ParameterType name -> Kind

-- | optional documentation
[ptDoc] :: ParameterType name -> Maybe String

-- | info for infix use
[ptFixity] :: ParameterType name -> Maybe Fixity

-- | number of the parameter
[ptNumber] :: ParameterType name -> !Int

-- | A value parameter
data ParameterFun name
ParameterFun :: Located name -> Schema name -> Maybe String -> Maybe Fixity -> ParameterFun name

-- | name of value parameter
[pfName] :: ParameterFun name -> Located name

-- | schema for parameter
[pfSchema] :: ParameterFun name -> Schema name

-- | optional documentation
[pfDoc] :: ParameterFun name -> Maybe String

-- | info for infix use
[pfFixity] :: ParameterFun name -> Maybe Fixity

-- | Input at the REPL, which can either be an expression or a let
--   statement.
data ReplInput name
ExprInput :: Expr name -> ReplInput name
LetInput :: Decl name -> ReplInput name
data Expr n

-- | 
--   x
--   
EVar :: n -> Expr n

-- | 
--   0x10
--   
ELit :: Literal -> Expr n

-- | 
--   -1
--   
ENeg :: Expr n -> Expr n

-- | 
--   ~1
--   
EComplement :: Expr n -> Expr n

-- | 
--   generate f
--   
EGenerate :: Expr n -> Expr n

-- | 
--   (1,2,3)
--   
ETuple :: [Expr n] -> Expr n

-- | 
--   { x = 1, y = 2 }
--   
ERecord :: [Named (Expr n)] -> Expr n

-- | 
--   e.l
--   
ESel :: Expr n -> Selector -> Expr n

-- | 
--   { r | x = e }
--   
EUpd :: Maybe (Expr n) -> [UpdField n] -> Expr n

-- | 
--   [1,2,3]
--   
EList :: [Expr n] -> Expr n

-- | 
--   [1, 5 .. 117 : t]
--   
EFromTo :: Type n -> Maybe (Type n) -> Type n -> Maybe (Type n) -> Expr n

-- | 
--   [1, 3 ...]
--   
EInfFrom :: Expr n -> Maybe (Expr n) -> Expr n

-- | 
--   [ 1 | x <- xs ]
--   
EComp :: Expr n -> [[Match n]] -> Expr n

-- | 
--   f x
--   
EApp :: Expr n -> Expr n -> Expr n

-- | 
--   f `{x = 8}, f`{8}
--   
EAppT :: Expr n -> [TypeInst n] -> Expr n

-- | 
--   if ok then e1 else e2
--   
EIf :: Expr n -> Expr n -> Expr n -> Expr n

-- | 
--   1 + x where { x = 2 }
--   
EWhere :: Expr n -> [Decl n] -> Expr n

-- | 
--   1 : [8]
--   
ETyped :: Expr n -> Type n -> Expr n

-- |  `(x + 1), x is a type
ETypeVal :: Type n -> Expr n

-- | 
--   \x y -> x
--   
EFun :: [Pattern n] -> Expr n -> Expr n

-- | position annotation
ELocated :: Expr n -> Range -> Expr n

-- |  splitAt x  (Introduced by NoPat)
ESplit :: Expr n -> Expr n

-- |  (e)  (Removed by Fixity)
EParens :: Expr n -> Expr n

-- |  a + b  (Removed by Fixity)
EInfix :: Expr n -> Located n -> Fixity -> Expr n -> Expr n

-- | Literals.
data Literal

-- | 0x10 (HexLit 2)
ECNum :: Integer -> NumInfo -> Literal

-- | 
--   "hello"
--   
ECString :: String -> Literal

-- | Infromation about the representation of a numeric constant.
data NumInfo

-- | n-digit binary literal
BinLit :: Int -> NumInfo

-- | n-digit octal literal
OctLit :: Int -> NumInfo

-- | overloaded decimal literal
DecLit :: NumInfo

-- | n-digit hex literal
HexLit :: Int -> NumInfo

-- | character literal
CharLit :: NumInfo

-- | polynomial literal
PolyLit :: Int -> NumInfo
data Match name

-- | p <- e
Match :: Pattern name -> Expr name -> Match name
MatchLet :: Bind name -> Match name
data Pattern n

-- | 
--   x
--   
PVar :: Located n -> Pattern n

-- | 
--   _
--   
PWild :: Pattern n

-- | 
--   (x,y,z)
--   
PTuple :: [Pattern n] -> Pattern n

-- | 
--   { x = (a,b,c), y = z }
--   
PRecord :: [Named (Pattern n)] -> Pattern n

-- | 
--   [ x, y, z ]
--   
PList :: [Pattern n] -> Pattern n

-- | 
--   x : [8]
--   
PTyped :: Pattern n -> Type n -> Pattern n

-- | 
--   (x # y)
--   
PSplit :: Pattern n -> Pattern n -> Pattern n

-- | Location information
PLocated :: Pattern n -> Range -> Pattern n

-- | Selectors are used for projecting from various components. Each
--   selector has an option spec to specify the shape of the thing that is
--   being selected. Currently, there is no surface syntax for list
--   selectors, but they are used during the desugaring of patterns.
data Selector

-- | Zero-based tuple selection. Optionally specifies the shape of the
--   tuple (one-based).
TupleSel :: Int -> Maybe Int -> Selector

-- | Record selection. Optionally specifies the shape of the record.
RecordSel :: Ident -> Maybe [Ident] -> Selector

-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> Maybe Int -> Selector
data TypeInst name
NamedInst :: Named (Type name) -> TypeInst name
PosInst :: Type name -> TypeInst name
data UpdField n

-- | non-empty list  x.y = e
UpdField :: UpdHow -> [Located Selector] -> Expr n -> UpdField n
data UpdHow
UpdSet :: UpdHow

-- | Are we setting or updating a field.
UpdFun :: UpdHow
data Located a
Located :: !Range -> !a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> !a

-- | A name with location information.
type LPName = Located PName

-- | A string with location information.
type LString = Located String

-- | An identifier with location information.
type LIdent = Located Ident
class NoPos t
noPos :: NoPos t => t -> t

-- | Conversational printing of kinds (e.g., to use in error
--   messages)
cppKind :: Kind -> Doc

-- | Display the thing selected by the selector, nicely.
ppSelector :: Selector -> Doc
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Program name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Module name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Module name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Module name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopDecl name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ReplInput name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ReplInput name)
instance GHC.Base.Functor Cryptol.Parser.AST.UpdField
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.UpdField n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.UpdField n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.UpdField n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.UpdField n)
instance GHC.Base.Functor Cryptol.Parser.AST.BindDef
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.BindDef name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.BindDef name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.BindDef name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.BindDef name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Bind name)
instance GHC.Base.Functor Cryptol.Parser.AST.Bind
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Bind name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Bind name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Bind name)
instance GHC.Base.Functor Cryptol.Parser.AST.Match
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Match name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Match name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Match name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Match name)
instance GHC.Base.Functor Cryptol.Parser.AST.Expr
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Expr n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Expr n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Expr n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Expr n)
instance GHC.Base.Functor Cryptol.Parser.AST.Decl
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Decl name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Decl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Decl name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Decl name)
instance GHC.Base.Functor Cryptol.Parser.AST.PropSyn
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.PropSyn n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.PropSyn n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.PropSyn n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.PropSyn n)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.PrimType name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.PrimType name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.PrimType name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.ParameterFun name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.ParameterFun name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ParameterFun name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ParameterFun name)
instance GHC.Base.Functor Cryptol.Parser.AST.Schema
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Schema n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Schema n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Schema n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Schema n)
instance GHC.Base.Functor Cryptol.Parser.AST.Prop
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Prop n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Prop n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Prop n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Prop n)
instance GHC.Base.Functor Cryptol.Parser.AST.TySyn
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TySyn n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TySyn n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TySyn n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TySyn n)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Newtype name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Newtype name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Newtype name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Newtype name)
instance GHC.Base.Functor Cryptol.Parser.AST.TypeInst
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TypeInst name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TypeInst name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TypeInst name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.TypeInst name)
instance GHC.Base.Functor Cryptol.Parser.AST.Pattern
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Pattern n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Pattern n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Pattern n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Pattern n)
instance GHC.Base.Functor Cryptol.Parser.AST.Type
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Type n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Type n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Type n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Type n)
instance GHC.Base.Functor Cryptol.Parser.AST.TParam
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TParam n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TParam n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TParam n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TParam n)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.ParameterType name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.ParameterType name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ParameterType name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ParameterType name)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Kind
instance GHC.Generics.Generic Cryptol.Parser.AST.Kind
instance GHC.Show.Show Cryptol.Parser.AST.Kind
instance GHC.Classes.Eq Cryptol.Parser.AST.Kind
instance GHC.Base.Functor Cryptol.Parser.AST.Named
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.Named a)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Named a)
instance Data.Traversable.Traversable Cryptol.Parser.AST.Named
instance Data.Foldable.Foldable Cryptol.Parser.AST.Named
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.Named a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.Named a)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.UpdHow
instance GHC.Generics.Generic Cryptol.Parser.AST.UpdHow
instance GHC.Show.Show Cryptol.Parser.AST.UpdHow
instance GHC.Classes.Eq Cryptol.Parser.AST.UpdHow
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Literal
instance GHC.Generics.Generic Cryptol.Parser.AST.Literal
instance GHC.Show.Show Cryptol.Parser.AST.Literal
instance GHC.Classes.Eq Cryptol.Parser.AST.Literal
instance Control.DeepSeq.NFData Cryptol.Parser.AST.NumInfo
instance GHC.Generics.Generic Cryptol.Parser.AST.NumInfo
instance GHC.Show.Show Cryptol.Parser.AST.NumInfo
instance GHC.Classes.Eq Cryptol.Parser.AST.NumInfo
instance Data.Traversable.Traversable Cryptol.Parser.AST.TopLevel
instance Data.Foldable.Foldable Cryptol.Parser.AST.TopLevel
instance GHC.Base.Functor Cryptol.Parser.AST.TopLevel
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopLevel a)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TopLevel a)
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.TopLevel a)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.ExportType
instance GHC.Generics.Generic Cryptol.Parser.AST.ExportType
instance GHC.Classes.Ord Cryptol.Parser.AST.ExportType
instance GHC.Show.Show Cryptol.Parser.AST.ExportType
instance GHC.Classes.Eq Cryptol.Parser.AST.ExportType
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Pragma
instance GHC.Generics.Generic Cryptol.Parser.AST.Pragma
instance GHC.Show.Show Cryptol.Parser.AST.Pragma
instance GHC.Classes.Eq Cryptol.Parser.AST.Pragma
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Import
instance GHC.Generics.Generic Cryptol.Parser.AST.Import
instance GHC.Show.Show Cryptol.Parser.AST.Import
instance GHC.Classes.Eq Cryptol.Parser.AST.Import
instance Control.DeepSeq.NFData Cryptol.Parser.AST.ImportSpec
instance GHC.Generics.Generic Cryptol.Parser.AST.ImportSpec
instance GHC.Show.Show Cryptol.Parser.AST.ImportSpec
instance GHC.Classes.Eq Cryptol.Parser.AST.ImportSpec
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.Position.Located t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Named t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos [t]
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (GHC.Maybe.Maybe t)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Program name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Module name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopDecl name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.PrimType name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.ParameterType name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.ParameterFun x)
instance Cryptol.Parser.AST.NoPos a => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Decl name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Newtype name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Bind name)
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pragma
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TySyn name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.PropSyn name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Expr name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.UpdField name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TypeInst name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Match name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Schema name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Prop name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Program name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Module name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Module name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopDecl name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopDecl name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Expr n)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Expr name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Bind name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Match name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Decl name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Decl name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Decl name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Bind name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.BindDef name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Expr name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.UpdField name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Match name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.PropSyn name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.PrimType name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.PrimType name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.ParameterFun name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.ParameterFun name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Schema name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Schema name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Schema name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Prop name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TySyn name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Newtype name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Newtype name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TypeInst name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Type name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.TParam name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.ParameterType name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.ParameterType name)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Kind
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Named a)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.UpdHow
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Literal
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pragma
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Import
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ImportSpec

-- | Utility functions that are also useful for translating programs from
--   previous Cryptol versions.
module Cryptol.Parser.Utils
translateExprToNumT :: Expr PName -> Maybe (Type PName)
widthIdent :: Ident

-- | This module defines the scoping rules for value- and type-level names
--   in Cryptol.
module Cryptol.Parser.Names

-- | The names defined by a newtype.
tnamesNT :: Newtype name -> ([Located name], ())

-- | The names defined and used by a group of mutually recursive
--   declarations.
namesDs :: Ord name => [Decl name] -> ([Located name], Set name)

-- | The names defined and used by a single declarations.
namesD :: Ord name => Decl name -> ([Located name], Set name)

-- | The names defined and used by a single declarations in such a way that
--   they cannot be duplicated in a file. For example, it is fine to use
--   x on the RHS of two bindings, but not on the LHS of two type
--   signatures.
allNamesD :: Ord name => Decl name -> [Located name]

-- | The names defined and used by a single binding.
namesB :: Ord name => Bind name -> ([Located name], Set name)
namesDef :: Ord name => BindDef name -> Set name

-- | The names used by an expression.
namesE :: Ord name => Expr name -> Set name
namesUF :: Ord name => UpdField name -> Set name

-- | The names defined by a group of patterns.
namesPs :: [Pattern name] -> [Located name]

-- | The names defined by a pattern. These will always be unqualified
--   names.
namesP :: Pattern name -> [Located name]

-- | The names defined and used by a match.
namesM :: Ord name => Match name -> ([Located name], Set name)

-- | The names defined and used by an arm of alist comprehension.
namesArm :: Ord name => [Match name] -> ([Located name], Set name)

-- | Remove some defined variables from a set of free variables.
boundLNames :: Ord name => [Located name] -> Set name -> Set name

-- | Remove some defined variables from a set of free variables.
boundNames :: Ord name => [name] -> Set name -> Set name

-- | Remove some defined variables from a set of free variables.
boundNamesSet :: Ord name => Set name -> Set name -> Set name

-- | The type names defined and used by a group of mutually recursive
--   declarations.
tnamesDs :: Ord name => [Decl name] -> ([Located name], Set name)

-- | The type names defined and used by a single declaration.
tnamesD :: Ord name => Decl name -> ([Located name], Set name)

-- | The type names used by a single binding.
tnamesB :: Ord name => Bind name -> Set name
tnamesDef :: Ord name => BindDef name -> Set name

-- | The type names used by an expression.
tnamesE :: Ord name => Expr name -> Set name
tnamesUF :: Ord name => UpdField name -> Set name
tnamesTI :: Ord name => TypeInst name -> Set name

-- | The type names used by a pattern.
tnamesP :: Ord name => Pattern name -> Set name

-- | The type names used by a match.
tnamesM :: Ord name => Match name -> Set name

-- | The type names used by a type schema.
tnamesS :: Ord name => Schema name -> Set name

-- | The type names used by a prop.
tnamesC :: Ord name => Prop name -> Set name

-- | Compute the type synonyms/type variables used by a type.
tnamesT :: Ord name => Type name -> Set name

-- | The purpose of this module is to convert all patterns to variable
--   patterns. It also eliminates pattern bindings by de-sugaring them into
--   Bind. Furthermore, here we associate signatures and pragmas
--   with the names to which they belong.
module Cryptol.Parser.NoPat
class RemovePatterns t

-- | Eliminate all patterns in a program.
removePatterns :: RemovePatterns t => t -> (t, [Error])
data Error
MultipleSignatures :: PName -> [Located (Schema PName)] -> Error
SignatureNoBind :: Located PName -> Schema PName -> Error
PragmaNoBind :: Located PName -> Pragma -> Error
MultipleFixities :: PName -> [Range] -> Error
FixityNoBind :: Located PName -> Error
MultipleDocs :: PName -> [Range] -> Error
instance Control.DeepSeq.NFData Cryptol.Parser.NoPat.Error
instance GHC.Generics.Generic Cryptol.Parser.NoPat.Error
instance GHC.Show.Show Cryptol.Parser.NoPat.Error
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Program Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Expr Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName]
instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM
instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error

module Cryptol.ModuleSystem.Exports
modExports :: Ord name => Module name -> ExportSpec name
data ExportSpec name
ExportSpec :: Set name -> Set name -> ExportSpec name
[eTypes] :: ExportSpec name -> Set name
[eBinds] :: ExportSpec name -> Set name

-- | Add a binding name to the export list, if it should be exported.
exportBind :: Ord name => TopLevel name -> ExportSpec name

-- | Add a type synonym name to the export list, if it should be exported.
exportType :: Ord name => TopLevel name -> ExportSpec name

-- | Check to see if a binding is exported.
isExportedBind :: Ord name => name -> ExportSpec name -> Bool

-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
instance GHC.Generics.Generic (Cryptol.ModuleSystem.Exports.ExportSpec name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.ModuleSystem.Exports.ExportSpec name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.ModuleSystem.Exports.ExportSpec name)
instance GHC.Classes.Ord name => GHC.Base.Semigroup (Cryptol.ModuleSystem.Exports.ExportSpec name)
instance GHC.Classes.Ord name => GHC.Base.Monoid (Cryptol.ModuleSystem.Exports.ExportSpec name)

-- | At present Alex generates code with too many warnings.
module Cryptol.Parser.Lexer

-- | Returns the tokens and the last position of the input that we
--   processed. The tokens include whte space tokens.
primLexer :: Config -> Text -> ([Located Token], Position)

-- | Returns the tokens in the last position of the input that we
--   processed. White space is removed, and layout processing is done as
--   requested. This stream is fed to the parser.
lexer :: Config -> Text -> ([Located Token], Position)
data Layout
Layout :: Layout
NoLayout :: Layout
data Token
Token :: !TokenT -> !Text -> Token
[tokenType] :: Token -> !TokenT
[tokenText] :: Token -> !Text
data TokenT

-- | value, base, number of digits
Num :: !Integer -> !Int -> !Int -> TokenT

-- | character literal
ChrLit :: !Char -> TokenT

-- | (qualified) identifier
Ident :: ![Text] -> !Text -> TokenT

-- | string literal
StrLit :: !String -> TokenT

-- | keyword
KW :: !TokenKW -> TokenT

-- | operator
Op :: !TokenOp -> TokenT

-- | symbol
Sym :: !TokenSym -> TokenT

-- | virtual token (for layout)
Virt :: !TokenV -> TokenT

-- | white space token
White :: !TokenW -> TokenT

-- | error token
Err :: !TokenErr -> TokenT
EOF :: TokenT

-- | Virtual tokens, inserted by layout processing.
data TokenV
VCurlyL :: TokenV
VCurlyR :: TokenV
VSemi :: TokenV
data TokenKW
KW_else :: TokenKW
KW_extern :: TokenKW
KW_fin :: TokenKW
KW_if :: TokenKW
KW_private :: TokenKW
KW_include :: TokenKW
KW_inf :: TokenKW
KW_lg2 :: TokenKW
KW_lengthFromThen :: TokenKW
KW_lengthFromThenTo :: TokenKW
KW_max :: TokenKW
KW_min :: TokenKW
KW_module :: TokenKW
KW_newtype :: TokenKW
KW_pragma :: TokenKW
KW_property :: TokenKW
KW_then :: TokenKW
KW_type :: TokenKW
KW_where :: TokenKW
KW_let :: TokenKW
KW_x :: TokenKW
KW_import :: TokenKW
KW_as :: TokenKW
KW_hiding :: TokenKW
KW_infixl :: TokenKW
KW_infixr :: TokenKW
KW_infix :: TokenKW
KW_primitive :: TokenKW
KW_parameter :: TokenKW
KW_constraint :: TokenKW
KW_Prop :: TokenKW
data TokenErr
UnterminatedComment :: TokenErr
UnterminatedString :: TokenErr
UnterminatedChar :: TokenErr
InvalidString :: TokenErr
InvalidChar :: TokenErr
LexicalError :: TokenErr
data TokenSym
Bar :: TokenSym
ArrL :: TokenSym
ArrR :: TokenSym
FatArrR :: TokenSym
Lambda :: TokenSym
EqDef :: TokenSym
Comma :: TokenSym
Semi :: TokenSym
Dot :: TokenSym
DotDot :: TokenSym
DotDotDot :: TokenSym
Colon :: TokenSym
BackTick :: TokenSym
ParenL :: TokenSym
ParenR :: TokenSym
BracketL :: TokenSym
BracketR :: TokenSym
CurlyL :: TokenSym
CurlyR :: TokenSym
TriL :: TokenSym
TriR :: TokenSym
Underscore :: TokenSym
data TokenW
BlockComment :: TokenW
LineComment :: TokenW
Space :: TokenW
DocStr :: TokenW
data Located a
Located :: !Range -> !a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> !a
data Config
Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config

-- | File that we are working on
[cfgSource] :: Config -> !FilePath

-- | Settings for layout processing
[cfgLayout] :: Config -> !Layout

-- | Preprocessor settings
[cfgPreProc] :: Config -> PreProc

-- | Implicit includes
[cfgAutoInclude] :: Config -> [FilePath]

-- | When we do layout processing should we add a vCurly (i.e., are we
--   parsing a list of things).
[cfgModuleScope] :: Config -> Bool
defaultConfig :: Config

module Cryptol.ModuleSystem.Name
data Name

-- | Information about the binding site of the name.
data NameInfo

-- | This name refers to a declaration from this module
Declared :: !ModName -> !NameSource -> NameInfo

-- | This name is a parameter (function or type)
Parameter :: NameInfo
data NameSource
SystemName :: NameSource
UserName :: NameSource
nameUnique :: Name -> Int
nameIdent :: Name -> Ident
nameInfo :: Name -> NameInfo
nameLoc :: Name -> Range
nameFixity :: Name -> Maybe Fixity
asPrim :: Name -> Maybe Ident

-- | Compare two names lexically.
cmpNameLexical :: Name -> Name -> Ordering

-- | Compare two names by the way they would be displayed.
cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering

-- | Pretty-print a name with its source location information.
ppLocName :: Name -> Doc

-- | Make a new name for a declaration.
mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name, Supply)

-- | Make a new parameter name.
mkParameter :: Ident -> Range -> Supply -> (Name, Supply)
toParamInstName :: Name -> Name
asParamName :: Name -> Name
paramModRecParam :: Name
class Monad m => FreshM m
liftSupply :: FreshM m => (Supply -> (a, Supply)) -> m a

-- | Retrieve the next unique from the supply.
nextUniqueM :: FreshM m => m Int

-- | A monad for easing the use of the supply.
data SupplyT m a
runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a, Supply)
data Supply

-- | This should only be used once at library initialization, and threaded
--   through the rest of the session. The supply is started at 0x1000 to
--   leave us plenty of room for names that the compiler needs to know
--   about (wired-in constants).
emptySupply :: Supply
nextUnique :: Supply -> (Int, Supply)

-- | A mapping from an identifier defined in some module to its real name.
data PrimMap
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
[primDecls] :: PrimMap -> Map Ident Name
[primTypes] :: PrimMap -> Map Ident Name

-- | It's assumed that we're looking things up that we know already exist,
--   so this will panic if it doesn't find the name.
lookupPrimDecl :: Ident -> PrimMap -> Name

-- | It's assumed that we're looking things up that we know already exist,
--   so this will panic if it doesn't find the name.
lookupPrimType :: Ident -> PrimMap -> Name
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.PrimMap
instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.PrimMap
instance GHC.Show.Show Cryptol.ModuleSystem.Name.PrimMap
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.Supply
instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.Supply
instance GHC.Show.Show Cryptol.ModuleSystem.Name.Supply
instance GHC.Show.Show Cryptol.ModuleSystem.Name.Name
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.Name
instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.Name
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.NameInfo
instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.NameInfo
instance GHC.Show.Show Cryptol.ModuleSystem.Name.NameInfo
instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.NameInfo
instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.NameSource
instance GHC.Show.Show Cryptol.ModuleSystem.Name.NameSource
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Name.NameSource
instance GHC.Generics.Generic Cryptol.ModuleSystem.Name.NameSource
instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.ExceptionT i m)
instance (GHC.Base.Monoid i, Cryptol.ModuleSystem.Name.FreshM m) => Cryptol.ModuleSystem.Name.FreshM (MonadLib.WriterT i m)
instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.ReaderT i m)
instance Cryptol.ModuleSystem.Name.FreshM m => Cryptol.ModuleSystem.Name.FreshM (MonadLib.StateT i m)
instance GHC.Base.Monad m => Cryptol.ModuleSystem.Name.FreshM (Cryptol.ModuleSystem.Name.SupplyT m)
instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Name.SupplyT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Name.SupplyT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Name.SupplyT m)
instance MonadLib.MonadT Cryptol.ModuleSystem.Name.SupplyT
instance MonadLib.BaseM m n => MonadLib.BaseM (Cryptol.ModuleSystem.Name.SupplyT m) n
instance MonadLib.RunM m (a, Cryptol.ModuleSystem.Name.Supply) r => MonadLib.RunM (Cryptol.ModuleSystem.Name.SupplyT m) a (Cryptol.ModuleSystem.Name.Supply -> r)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Cryptol.ModuleSystem.Name.SupplyT m)
instance GHC.Classes.Eq Cryptol.ModuleSystem.Name.Name
instance GHC.Classes.Ord Cryptol.ModuleSystem.Name.Name
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Name.Name
instance Cryptol.Utils.PP.PPName Cryptol.ModuleSystem.Name.Name

module Cryptol.TypeCheck.TCon

-- | This is used for pretty prinitng. XXX: it would be nice to just rely
--   in the info from the Prelude.
infixPrimTy :: TCon -> Maybe (Ident, Fixity)
builtInType :: Name -> Maybe TCon

-- | Kinds, classify types.
data Kind
KType :: Kind
KNum :: Kind
KProp :: Kind
(:->) :: Kind -> Kind -> Kind
infixr 5 :->
class HasKind t
kindOf :: HasKind t => t -> Kind

-- | Type constants.
data TCon
TC :: TC -> TCon
PC :: PC -> TCon
TF :: TFun -> TCon
TError :: Kind -> TCErrorMessage -> TCon

-- | Predicate symbols. If you add additional user-visible constructors,
--   please update primTys.
data PC

-- | 
--   _ == _
--   
PEqual :: PC

-- | 
--   _ /= _
--   
PNeq :: PC

-- | 
--   _ >= _
--   
PGeq :: PC

-- | 
--   fin _
--   
PFin :: PC

-- | Has sel type field does not appear in schemas
PHas :: Selector -> PC

-- | 
--   Zero _
--   
PZero :: PC

-- | 
--   Logic _
--   
PLogic :: PC

-- | 
--   Arith _
--   
PArith :: PC

-- | 
--   Cmp _
--   
PCmp :: PC

-- | 
--   SignedCmp _
--   
PSignedCmp :: PC

-- | 
--   Literal _ _
--   
PLiteral :: PC

-- | This is useful when simplifying things in place
PAnd :: PC

-- | Ditto
PTrue :: PC

-- | 1-1 constants. If you add additional user-visible constructors, please
--   update primTys.
data TC

-- | Numbers
TCNum :: Integer -> TC

-- | Inf
TCInf :: TC

-- | Bit
TCBit :: TC

-- | Integer
TCInteger :: TC

-- | 
--   Z _
--   
TCIntMod :: TC

-- | 
--   [_] _
--   
TCSeq :: TC

-- | 
--   _ -> _
--   
TCFun :: TC

-- | 
--   (_, _, _)
--   
TCTuple :: Int -> TC

-- | An abstract type
TCAbstract :: UserTC -> TC

-- | user-defined, T
TCNewtype :: UserTC -> TC
data UserTC
UserTC :: Name -> Kind -> UserTC
data TCErrorMessage
TCErrorMessage :: !String -> TCErrorMessage
[tcErrorMessage] :: TCErrorMessage -> !String

-- | Built-in type functions. If you add additional user-visible
--   constructors, please update primTys in
--   Cryptol.Prims.Types.
data TFun

-- | 
--   : Num -> Num -> Num
--   
TCAdd :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCSub :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMul :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCDiv :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMod :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCExp :: TFun

-- | 
--   : Num -> Num
--   
TCWidth :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMin :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMax :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCCeilDiv :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCCeilMod :: TFun

-- |  : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9
--   ] :: [lengthFromThenTo 1 5 9][b]
TCLenFromThenTo :: TFun
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.TCon
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.TCon
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.TCon
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.TCon
instance GHC.Show.Show Cryptol.TypeCheck.TCon.TCon
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.TFun
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.TFun
instance GHC.Enum.Enum Cryptol.TypeCheck.TCon.TFun
instance GHC.Enum.Bounded Cryptol.TypeCheck.TCon.TFun
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.TFun
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.TFun
instance GHC.Show.Show Cryptol.TypeCheck.TCon.TFun
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.TCErrorMessage
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.TCErrorMessage
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.TCErrorMessage
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.TCErrorMessage
instance GHC.Show.Show Cryptol.TypeCheck.TCon.TCErrorMessage
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.TC
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.TC
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.TC
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.TC
instance GHC.Show.Show Cryptol.TypeCheck.TCon.TC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.UserTC
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.UserTC
instance GHC.Show.Show Cryptol.TypeCheck.TCon.UserTC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.PC
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.PC
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.PC
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.PC
instance GHC.Show.Show Cryptol.TypeCheck.TCon.PC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.TCon.Kind
instance GHC.Generics.Generic Cryptol.TypeCheck.TCon.Kind
instance GHC.Show.Show Cryptol.TypeCheck.TCon.Kind
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.Kind
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.Kind
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.TCon.TCon
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.TCon
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.TCon.TFun
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.TFun
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.TCErrorMessage
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.TCon.TC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.TC
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.TCon.UserTC
instance GHC.Classes.Eq Cryptol.TypeCheck.TCon.UserTC
instance GHC.Classes.Ord Cryptol.TypeCheck.TCon.UserTC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.UserTC
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.TCon.PC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.PC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.TCon.Kind

module Cryptol.TypeCheck.Type
class FVS t
fvs :: FVS t => t -> Set TVar

-- | The type is "simple" (i.e., it contains no type functions).
type SType = Type

-- | Information about an abstract type.
data AbstractType
AbstractType :: Name -> Kind -> ([TParam], [Prop]) -> Maybe Fixity -> Maybe String -> AbstractType
[atName] :: AbstractType -> Name
[atKind] :: AbstractType -> Kind
[atCtrs] :: AbstractType -> ([TParam], [Prop])
[atFixitiy] :: AbstractType -> Maybe Fixity
[atDoc] :: AbstractType -> Maybe String

-- | Named records
data Newtype
Newtype :: Name -> [TParam] -> [Prop] -> [(Ident, Type)] -> Maybe String -> Newtype
[ntName] :: Newtype -> Name
[ntParams] :: Newtype -> [TParam]
[ntConstraints] :: Newtype -> [Prop]
[ntFields] :: Newtype -> [(Ident, Type)]
[ntDoc] :: Newtype -> Maybe String

-- | Type synonym.
data TySyn
TySyn :: Name -> [TParam] -> [Prop] -> Type -> !Maybe String -> TySyn

-- | Name
[tsName] :: TySyn -> Name

-- | Parameters
[tsParams] :: TySyn -> [TParam]

-- | Ensure body is OK
[tsConstraints] :: TySyn -> [Prop]

-- | Definition
[tsDef] :: TySyn -> Type

-- | Documentation
[tsDoc] :: TySyn -> !Maybe String

-- | The type is supposed to be of kind KProp
type Prop = Type
data TVarSource

-- | Name of module parameter
TVFromModParam :: Name -> TVarSource

-- | A variable in a signature
TVFromSignature :: Name -> TVarSource
TypeWildCard :: TVarSource
TypeOfRecordField :: Ident -> TVarSource
TypeOfTupleField :: Int -> TVarSource
TypeOfSeqElement :: TVarSource
LenOfSeq :: TVarSource
TypeParamInstNamed :: Name -> Ident -> TVarSource
TypeParamInstPos :: Name -> Int -> TVarSource
DefinitionOf :: Name -> TVarSource
LenOfCompGen :: TVarSource
TypeOfArg :: Maybe Int -> TVarSource
TypeOfRes :: TVarSource
TypeErrorPlaceHolder :: TVarSource
data TVarInfo
TVarInfo :: Range -> TVarSource -> TVarInfo

-- | Source code that gave rise
[tvarSource] :: TVarInfo -> Range

-- | Description
[tvarDesc] :: TVarInfo -> TVarSource

-- | Type variables.
data TVar

-- | Unique, kind, ids of bound type variables that are in scope The last
--   field gives us some infor for nicer warnings/errors.
TVFree :: !Int -> Kind -> Set TParam -> TVarInfo -> TVar
TVBound :: {-# UNPACK #-} !TParam -> TVar

-- | The internal representation of types. These are assumed to be kind
--   correct.
data Type

-- | Type constant with args
TCon :: !TCon -> ![Type] -> Type

-- | Type variable (free or bound)
TVar :: TVar -> Type

-- | This is just a type annotation, for a type that was written as a type
--   synonym. It is useful so that we can use it to report nicer errors.
--   Example: `TUser T ts t` is really just the type t that was
--   written as `T ts` by the user.
TUser :: !Name -> ![Type] -> !Type -> Type

-- | Record type
TRec :: ![(Ident, Type)] -> Type
data TPFlavor
TPModParam :: Name -> TPFlavor
TPOther :: Maybe Name -> TPFlavor

-- | Type parameters.
data TParam
TParam :: !Int -> Kind -> TPFlavor -> !TVarInfo -> TParam

-- | Parameter identifier
[tpUnique] :: TParam -> !Int

-- | Kind of parameter
[tpKind] :: TParam -> Kind

-- | What sort of type parameter is this
[tpFlav] :: TParam -> TPFlavor

-- | A description for better messages.
[tpInfo] :: TParam -> !TVarInfo

-- | The types of polymorphic values.
data Schema
Forall :: [TParam] -> [Prop] -> Type -> Schema
[sVars] :: Schema -> [TParam]
[sProps] :: Schema -> [Prop]
[sType] :: Schema -> Type
tMono :: Type -> Schema
isMono :: Schema -> Maybe Type
schemaParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
tpfName :: TPFlavor -> Maybe Name
tpName :: TParam -> Maybe Name
tvInfo :: TVar -> TVarInfo

-- | Get the names of something that is related to the tvar.
tvSourceName :: TVarSource -> Maybe Name
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
newtypeConType :: Newtype -> Schema
abstractTypeTC :: AbstractType -> TCon
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsError :: Type -> Maybe TCErrorMessage
tIsNat' :: Type -> Maybe Nat'
tIsNum :: Type -> Maybe Integer
tIsInf :: Type -> Bool
tIsVar :: Type -> Maybe TVar
tIsFun :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsBit :: Type -> Bool
tIsInteger :: Type -> Bool
tIsIntMod :: Type -> Maybe Type
tIsTuple :: Type -> Maybe [Type]
tIsRec :: Type -> Maybe [(Ident, Type)]
tIsBinFun :: TFun -> Type -> Maybe (Type, Type)

-- | Split up repeated occurances of the given binary type-level function.
tSplitFun :: TFun -> Type -> [Type]
pIsFin :: Prop -> Maybe Type
pIsGeq :: Prop -> Maybe (Type, Type)
pIsEq :: Prop -> Maybe (Type, Type)
pIsZero :: Prop -> Maybe Type
pIsLogic :: Prop -> Maybe Type
pIsArith :: Prop -> Maybe Type
pIsCmp :: Prop -> Maybe Type
pIsSignedCmp :: Prop -> Maybe Type
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsTrue :: Prop -> Bool
pIsWidth :: Prop -> Maybe Type
tNum :: Integral a => a -> Type
tZero :: Type
tOne :: Type
tTwo :: Type
tInf :: Type
tNat' :: Nat' -> Type
tAbstract :: UserTC -> [Type] -> Type
tBit :: Type
tInteger :: Type
tIntMod :: Type -> Type
tWord :: Type -> Type
tSeq :: Type -> Type -> Type
tChar :: Type
tString :: Int -> Type
tRec :: [(Ident, Type)] -> Type
tTuple :: [Type] -> Type
newtypeTyCon :: Newtype -> TCon

-- | Make a function type.
tFun :: Type -> Type -> Type
infixr 5 `tFun`

-- | Eliminate outermost type synonyms.
tNoUser :: Type -> Type

-- | Make a malformed numeric type.
tBadNumber :: TCErrorMessage -> Type

-- | Make an error value of the given type.
tError :: Kind -> TCErrorMessage -> Type
tf1 :: TFun -> Type -> Type
tf2 :: TFun -> Type -> Type -> Type
tf3 :: TFun -> Type -> Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type

-- | Equality for numeric types.
(=#=) :: Type -> Type -> Prop
infix 4 =#=
(=/=) :: Type -> Type -> Prop
pZero :: Type -> Prop
pLogic :: Type -> Prop
pArith :: Type -> Prop
pCmp :: Type -> Prop
pSignedCmp :: Type -> Prop
pLiteral :: Type -> Type -> Prop

-- | Make a greater-than-or-equal-to constraint.
(>==) :: Type -> Type -> Prop
infix 4 >==

-- | A Has constraint, used for tuple and record selection.
pHas :: Selector -> Type -> Type -> Prop
pTrue :: Prop
pAnd :: [Prop] -> Prop
pSplitAnd :: Prop -> [Prop]
pFin :: Type -> Prop

-- | Make a malformed property.
pError :: TCErrorMessage -> Prop
noFreeVariables :: FVS t => t -> Bool
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
pickTVarName :: Kind -> TVarSource -> Int -> Doc
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.AbstractType
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.AbstractType
instance GHC.Show.Show Cryptol.TypeCheck.Type.AbstractType
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Newtype
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Newtype
instance GHC.Show.Show Cryptol.TypeCheck.Type.Newtype
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TySyn
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TySyn
instance GHC.Show.Show Cryptol.TypeCheck.Type.TySyn
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Schema
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Schema
instance GHC.Show.Show Cryptol.TypeCheck.Type.Schema
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Schema
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Type
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Type
instance GHC.Show.Show Cryptol.TypeCheck.Type.Type
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVar
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVar
instance GHC.Show.Show Cryptol.TypeCheck.Type.TVar
instance GHC.Show.Show Cryptol.TypeCheck.Type.TParam
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TParam
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TParam
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVarInfo
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVarInfo
instance GHC.Show.Show Cryptol.TypeCheck.Type.TVarInfo
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVarSource
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVarSource
instance GHC.Show.Show Cryptol.TypeCheck.Type.TVarSource
instance GHC.Show.Show Cryptol.TypeCheck.Type.TPFlavor
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TPFlavor
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TPFlavor
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS (GHC.Maybe.Maybe a)
instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS [a]
instance (Cryptol.TypeCheck.Type.FVS a, Cryptol.TypeCheck.Type.FVS b) => Cryptol.TypeCheck.Type.FVS (a, b)
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Schema
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.Type.Newtype
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Newtype
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Newtype)
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.Type.TySyn
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TySyn
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TySyn)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Schema
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Schema)
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.Type.Type
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Type
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.Type
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Type)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.Type.TVar
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TVar
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TVar
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TVar)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVar
instance Cryptol.TypeCheck.TCon.HasKind Cryptol.TypeCheck.Type.TParam
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TParam
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TParam
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TParam
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TParam)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVarInfo
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVarSource

module Cryptol.TypeCheck.AST
data DeclDef
DPrim :: DeclDef
DExpr :: Expr -> DeclDef
data Decl
Decl :: !Name -> Schema -> DeclDef -> [Pragma] -> !Bool -> Maybe Fixity -> Maybe String -> Decl
[dName] :: Decl -> !Name
[dSignature] :: Decl -> Schema
[dDefinition] :: Decl -> DeclDef
[dPragmas] :: Decl -> [Pragma]
[dInfix] :: Decl -> !Bool
[dFixity] :: Decl -> Maybe Fixity
[dDoc] :: Decl -> Maybe String
data DeclGroup

-- | Mutually recursive declarations
Recursive :: [Decl] -> DeclGroup

-- | Non-recursive declaration
NonRecursive :: Decl -> DeclGroup
data Match

-- | Type arguments are the length and element type of the sequence
--   expression
From :: Name -> Type -> Type -> Expr -> Match
Let :: Decl -> Match
data Expr

-- | List value (with type of elements)
EList :: [Expr] -> Type -> Expr

-- | Tuple value
ETuple :: [Expr] -> Expr

-- | Record value
ERec :: [(Ident, Expr)] -> Expr

-- | Elimination for tuplerecordlist
ESel :: Expr -> Selector -> Expr

-- | Change the value of a field.
ESet :: Expr -> Selector -> Expr -> Expr

-- | If-then-else
EIf :: Expr -> Expr -> Expr -> Expr

-- | List comprehensions The types cache the length of the sequence and its
--   element type.
EComp :: Type -> Type -> Expr -> [[Match]] -> Expr

-- | Use of a bound variable
EVar :: Name -> Expr

-- | Function Value
ETAbs :: TParam -> Expr -> Expr

-- | Type application
ETApp :: Expr -> Type -> Expr

-- | Function application
EApp :: Expr -> Expr -> Expr

-- | Function value
EAbs :: Name -> Type -> Expr -> Expr

-- | Proof abstraction. Because we don't keep proofs around we don't need
--   to name the assumption, but we still need to record the assumption.
--   The assumption is the Type term, which should be of kind
--   KProp.
EProofAbs :: Prop -> Expr -> Expr

-- | If `e : p =&gt; t`, then `EProofApp e : t`, as long as we can prove
--   p.
--   
--   We don't record the actual proofs, as they are not used for anything.
--   It may be nice to keep them around for sanity checking.
EProofApp :: Expr -> Expr
EWhere :: Expr -> [DeclGroup] -> Expr

-- | A value parameter of a module.
data ModVParam
ModVParam :: Name -> Schema -> Maybe String -> Maybe Fixity -> ModVParam
[mvpName] :: ModVParam -> Name
[mvpType] :: ModVParam -> Schema
[mvpDoc] :: ModVParam -> Maybe String
[mvpFixity] :: ModVParam -> Maybe Fixity

-- | A type parameter of a module.
data ModTParam
ModTParam :: Name -> Kind -> !Int -> Maybe String -> ModTParam
[mtpName] :: ModTParam -> Name
[mtpKind] :: ModTParam -> Kind

-- | The number of the parameter in the module This is used when we move
--   parameters from the module level to individual declarations (type
--   synonyms in particular)
[mtpNumber] :: ModTParam -> !Int
[mtpDoc] :: ModTParam -> Maybe String

-- | A Cryptol module.
data Module
Module :: !ModName -> ExportSpec Name -> [Import] -> Map Name TySyn -> Map Name Newtype -> Map Name AbstractType -> Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> [DeclGroup] -> Module
[mName] :: Module -> !ModName
[mExports] :: Module -> ExportSpec Name
[mImports] :: Module -> [Import]

-- | This is just the type-level type synonyms of a module.
[mTySyns] :: Module -> Map Name TySyn
[mNewtypes] :: Module -> Map Name Newtype
[mPrimTypes] :: Module -> Map Name AbstractType
[mParamTypes] :: Module -> Map Name ModTParam
[mParamConstraints] :: Module -> [Located Prop]
[mParamFuns] :: Module -> Map Name ModVParam
[mDecls] :: Module -> [DeclGroup]

-- | Is this a parameterized module?
isParametrizedModule :: Module -> Bool
mtpParam :: ModTParam -> TParam
groupDecls :: DeclGroup -> [Decl]

-- | Construct a primitive, given a map to the unique names of the Cryptol
--   module.
ePrim :: PrimMap -> Ident -> Expr

-- | Make an expression that is error pre-applied to a type and a
--   message.
eError :: PrimMap -> Type -> String -> Expr
eString :: PrimMap -> String -> Expr
eChar :: PrimMap -> Char -> Expr
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitAbs :: Expr -> Maybe ((Name, Type), Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitTApp :: Expr -> Maybe (Type, Expr)
splitProofApp :: Expr -> Maybe ((), Expr)

-- | Deconstruct an expression, typically polymorphic, into the types and
--   proofs to which it is applied. Since we don't store the proofs, we
--   just return the number of proof applications. The first type is the
--   one closest to the expr.
splitExprInst :: Expr -> (Expr, [Type], Int)
data Name

-- | Built-in type functions. If you add additional user-visible
--   constructors, please update primTys in
--   Cryptol.Prims.Types.
data TFun

-- | 
--   : Num -> Num -> Num
--   
TCAdd :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCSub :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMul :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCDiv :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMod :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCExp :: TFun

-- | 
--   : Num -> Num
--   
TCWidth :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMin :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCMax :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCCeilDiv :: TFun

-- | 
--   : Num -> Num -> Num
--   
TCCeilMod :: TFun

-- |  : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9
--   ] :: [lengthFromThenTo 1 5 9][b]
TCLenFromThenTo :: TFun

-- | Selectors are used for projecting from various components. Each
--   selector has an option spec to specify the shape of the thing that is
--   being selected. Currently, there is no surface syntax for list
--   selectors, but they are used during the desugaring of patterns.
data Selector

-- | Zero-based tuple selection. Optionally specifies the shape of the
--   tuple (one-based).
TupleSel :: Int -> Maybe Int -> Selector

-- | Record selection. Optionally specifies the shape of the record.
RecordSel :: Ident -> Maybe [Ident] -> Selector

-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> Maybe Int -> Selector

-- | An import declaration.
data Import
Import :: !ModName -> Maybe ModName -> Maybe ImportSpec -> Import
[iModule] :: Import -> !ModName
[iAs] :: Import -> Maybe ModName
[iSpec] :: Import -> Maybe ImportSpec

-- | The list of names following an import.
--   
--   INVARIANT: All of the Name entries in the list are expected
--   to be unqualified names; the QName or NewName
--   constructors should not be present.
data ImportSpec
Hiding :: [Ident] -> ImportSpec
Only :: [Ident] -> ImportSpec

-- | Export information for a declaration.
data ExportType
Public :: ExportType
Private :: ExportType
data ExportSpec name
ExportSpec :: Set name -> Set name -> ExportSpec name
[eTypes] :: ExportSpec name -> Set name
[eBinds] :: ExportSpec name -> Set name

-- | Check to see if a binding is exported.
isExportedBind :: Ord name => name -> ExportSpec name -> Bool

-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma
data Fixity
Fixity :: !Assoc -> !Int -> Fixity
[fAssoc] :: Fixity -> !Assoc
[fLevel] :: Fixity -> !Int

-- | A mapping from an identifier defined in some module to its real name.
data PrimMap
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
[primDecls] :: PrimMap -> Map Ident Name
[primTypes] :: PrimMap -> Map Ident Name
data TCErrorMessage
TCErrorMessage :: !String -> TCErrorMessage
[tcErrorMessage] :: TCErrorMessage -> !String
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Module
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Module
instance GHC.Show.Show Cryptol.TypeCheck.AST.Module
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Match
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Match
instance GHC.Show.Show Cryptol.TypeCheck.AST.Match
instance GHC.Show.Show Cryptol.TypeCheck.AST.Decl
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Decl
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Decl
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclGroup
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclGroup
instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclGroup
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Expr
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Expr
instance GHC.Show.Show Cryptol.TypeCheck.AST.Expr
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclDef
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclDef
instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclDef
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.ModVParam
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.ModVParam
instance GHC.Show.Show Cryptol.TypeCheck.AST.ModVParam
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.ModTParam
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.ModTParam
instance GHC.Show.Show Cryptol.TypeCheck.AST.ModTParam
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Module
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Module)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Expr)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Expr
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Match)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Match
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclGroup)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Decl)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclDef)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Decl

module Cryptol.TypeCheck.TypeMap
data TypeMap a
TM :: Map TVar a -> Map TCon (List TypeMap a) -> Map [Ident] (List TypeMap a) -> TypeMap a
[tvar] :: TypeMap a -> Map TVar a
[tcon] :: TypeMap a -> Map TCon (List TypeMap a)
[trec] :: TypeMap a -> Map [Ident] (List TypeMap a)
type TypesMap = List TypeMap
class TrieMap m k | m -> k
emptyTM :: TrieMap m k => m a
nullTM :: TrieMap m k => m a -> Bool
lookupTM :: TrieMap m k => k -> m a -> Maybe a
alterTM :: TrieMap m k => k -> (Maybe a -> Maybe a) -> m a -> m a
unionTM :: TrieMap m k => (a -> a -> a) -> m a -> m a -> m a
toListTM :: TrieMap m k => m a -> [(k, a)]
mapMaybeWithKeyTM :: TrieMap m k => (k -> a -> Maybe b) -> m a -> m b
insertTM :: TrieMap m k => k -> a -> m a -> m a
insertWithTM :: TrieMap m k => (a -> a -> a) -> k -> a -> m a -> m a
membersTM :: TrieMap m k => m a -> [a]
mapTM :: TrieMap m k => (a -> b) -> m a -> m b
mapWithKeyTM :: TrieMap m k => (k -> a -> b) -> m a -> m b
mapMaybeTM :: TrieMap m k => (a -> Maybe b) -> m a -> m b
data List m a
L :: Maybe a -> m (List m a) -> List m a
[nil] :: List m a -> Maybe a
[cons] :: List m a -> m (List m a)
instance GHC.Base.Functor Cryptol.TypeCheck.TypeMap.TypeMap
instance GHC.Base.Functor m => GHC.Base.Functor (Cryptol.TypeCheck.TypeMap.List m)
instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.TypeCheck.TypeMap.TypeMap Cryptol.TypeCheck.Type.Type
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.TypeMap.TypeMap a)
instance Cryptol.TypeCheck.TypeMap.TrieMap m a => Cryptol.TypeCheck.TypeMap.TrieMap (Cryptol.TypeCheck.TypeMap.List m) [a]
instance GHC.Classes.Ord a => Cryptol.TypeCheck.TypeMap.TrieMap (Data.Map.Internal.Map a) a

-- | An interval interpretation of types.
module Cryptol.TypeCheck.Solver.Numeric.Interval

-- | Only meaningful for numeric types
typeInterval :: Map TVar Interval -> Type -> Interval
tvarInterval :: Map TVar Interval -> TVar -> Interval
data IntervalUpdate
NoChange :: IntervalUpdate
InvalidInterval :: TVar -> IntervalUpdate
NewIntervals :: Map TVar Interval -> IntervalUpdate
updateInterval :: (TVar, Interval) -> Map TVar Interval -> IntervalUpdate
computePropIntervals :: Map TVar Interval -> [Prop] -> IntervalUpdate

-- | What we learn about variables from a single prop.
propInterval :: Map TVar Interval -> Prop -> [(TVar, Interval)]
data Interval
Interval :: Nat' -> Maybe Nat' -> Interval

-- | lower bound (inclusive)
[iLower] :: Interval -> Nat'

-- | upper bound (inclusive) If there is no upper bound, then all *natural*
--   numbers.
[iUpper] :: Interval -> Maybe Nat'
ppIntervals :: Map TVar Interval -> Doc
ppInterval :: Interval -> Doc
iIsExact :: Interval -> Maybe Nat'
iIsFin :: Interval -> Bool

-- | Finite positive number. [1 .. inf).
iIsPosFin :: Interval -> Bool

-- | Returns True when the intervals definitely overlap, and
--   False otherwise.
iOverlap :: Interval -> Interval -> Bool

-- | Intersect two intervals, yielding a new one that describes the space
--   where they overlap. If the two intervals are disjoint, the result will
--   be Nothing.
iIntersect :: Interval -> Interval -> Maybe Interval

-- | Any value
iAny :: Interval

-- | Any finite value
iAnyFin :: Interval

-- | Exactly this value
iConst :: Nat' -> Interval
iAdd :: Interval -> Interval -> Interval
iMul :: Interval -> Interval -> Interval
iExp :: Interval -> Interval -> Interval
iMin :: Interval -> Interval -> Interval
iMax :: Interval -> Interval -> Interval
iSub :: Interval -> Interval -> Interval
iDiv :: Interval -> Interval -> Interval
iMod :: Interval -> Interval -> Interval
iCeilDiv :: Interval -> Interval -> Interval
iCeilMod :: Interval -> Interval -> Interval
iWidth :: Interval -> Interval
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.Interval.IntervalUpdate
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.Interval.Interval
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.Interval.Interval

module Cryptol.TypeCheck.Solver.Types
type Ctxt = Map TVar Interval
data Solved

-- | Solved, assuming the sub-goals.
SolvedIf :: [Prop] -> Solved

-- | We could not solve the goal.
Unsolved :: Solved

-- | The goal can never be solved.
Unsolvable :: TCErrorMessage -> Solved
elseTry :: Solved -> Solved -> Solved
solveOpts :: [Solved] -> Solved
matchThen :: Maybe a -> (a -> Solved) -> Solved
guarded :: Bool -> Solved -> Solved
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Types.Solved
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Solver.Types.Solved

-- | Simplification of fin constraints.
module Cryptol.TypeCheck.Solver.Numeric.Fin
cryIsFin :: Map TVar Interval -> Prop -> Solved
cryIsFinType :: Map TVar Interval -> Type -> Solved

module Cryptol.TypeCheck.Parseable
class ShowParseable t
showParseable :: ShowParseable t => t -> Doc
maybeNameDoc :: Maybe Name -> Doc
class ShowParseable t
showParseable :: ShowParseable t => t -> Doc
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Expr
instance (Cryptol.TypeCheck.Parseable.ShowParseable a, Cryptol.TypeCheck.Parseable.ShowParseable b) => Cryptol.TypeCheck.Parseable.ShowParseable (a, b)
instance Cryptol.TypeCheck.Parseable.ShowParseable GHC.Types.Int
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.Utils.Ident.Ident
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.Parser.Selector.Selector
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Match
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.Decl
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable [a]
instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable (GHC.Maybe.Maybe a)
instance Cryptol.TypeCheck.Parseable.ShowParseable a => Cryptol.TypeCheck.Parseable.ShowParseable (Cryptol.Parser.Position.Located a)
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.TypeCheck.Type.TParam
instance Cryptol.TypeCheck.Parseable.ShowParseable Cryptol.ModuleSystem.Name.Name

module Cryptol.IR.FreeVars
class FreeVars e
freeVars :: FreeVars e => e -> Deps
data Deps
Deps :: Set Name -> Set Name -> Set TParam -> Deps

-- | Undefined value names
[valDeps] :: Deps -> Set Name

-- | Undefined type names (from newtype)
[tyDeps] :: Deps -> Set Name

-- | Undefined type params (e.d. mod params)
[tyParams] :: Deps -> Set TParam
class Defs d
defs :: Defs d => d -> Set Name

-- | Dependencies of top-level declarations in a module. These are
--   dependencies on module parameters or things defined outside the
--   module.
moduleDeps :: Module -> Map Name Deps

-- | Compute the transitive closure of the given dependencies.
transDeps :: Map Name Deps -> Map Name Deps
instance GHC.Classes.Eq Cryptol.IR.FreeVars.Deps
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Expr
instance Cryptol.IR.FreeVars.Defs a => Cryptol.IR.FreeVars.Defs [a]
instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.Decl
instance Cryptol.IR.FreeVars.Defs Cryptol.TypeCheck.AST.Match
instance Cryptol.IR.FreeVars.FreeVars e => Cryptol.IR.FreeVars.FreeVars [e]
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Decl
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.AST.Match
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Schema
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Type
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.TVar
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.TCon.TCon
instance Cryptol.IR.FreeVars.FreeVars Cryptol.TypeCheck.Type.Newtype
instance GHC.Base.Semigroup Cryptol.IR.FreeVars.Deps
instance GHC.Base.Monoid Cryptol.IR.FreeVars.Deps

-- | This module implements a transformation, which tries to avoid
--   exponential slow down in some cases. What's the problem? Consider the
--   following (common) patterns:
--   
--   fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]
--   
--   The type of fibs is:
--   
--   {a} (a >= 1, fin a) => [inf][a]
--   
--   Here a is the number of bits to be used in the values
--   computed by fibs. When we evaluate fibs, a
--   becomes a parameter to fibs, which works except that now
--   fibs is a function, and we don't get any of the memoization
--   we might expect! What looked like an efficient implementation has all
--   of a sudden become exponential!
--   
--   Note that this is only a problem for polymorphic values: if
--   fibs was already a function, it would not be that surprising
--   that it does not get cached.
--   
--   So, to avoid this, we try to spot recursive polymorphic values, where
--   the recursive occurrences have the exact same type parameters as the
--   definition. For example, this is the case in fibs: each
--   recursive call to fibs is instantiated with exactly the same
--   type parameter (i.e., a). The rewrite we do is as follows:
--   
--   fibs : {a} (a >= 1, fin a) => [inf][a] fibs = {a} (a >= 1,
--   fin a) -> fibs' where fibs' : [inf][a] fibs' = [0,1] # [ x + y | x
--   <- fibs', y <- drop`{1} fibs' ]
--   
--   After the rewrite, the recursion is monomorphic (i.e., we are always
--   using the same type). As a result, fibs` is an ordinary
--   recursive value, where we get the benefit of caching.
--   
--   The rewrite is a bit more complex, when there are multiple mutually
--   recursive functions. Here is an example:
--   
--   zig : {a} (a >= 2, fin a) => [inf][a] zig = [1] # zag
--   
--   zag : {a} (a >= 2, fin a) => [inf][a] zag = [2] # zig
--   
--   This gets rewritten to:
--   
--   newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a]) newName =
--   {a} (a >= 2, fin a) -> (zig', zag') where zig' : [inf][a] zig' =
--   [1] # zag'
--   
--   zag' : [inf][a] zag' = [2] # zig'
--   
--   zig : {a} (a >= 2, fin a) => [inf][a] zig = {a} (a >= 2, fin
--   a) -> (newName a <> <> ).1
--   
--   zag : {a} (a >= 2, fin a) => [inf][a] zag = {a} (a >= 2, fin
--   a) -> (newName a <> <> ).2
--   
--   NOTE: We are assuming that no capture would occur with binders. For
--   values, this is because we replaces things with freshly chosen
--   variables. For types, this should be because there should be no
--   shadowing in the types. XXX: Make sure that this really is the case
--   for types!!
module Cryptol.Transform.MonoValues

-- | Note that this assumes that this pass will be run only once for each
--   module, otherwise we will get name collisions.
rewModule :: Supply -> Module -> (Module, Supply)
instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.Transform.MonoValues.RewMap' (Cryptol.ModuleSystem.Name.Name, [Cryptol.TypeCheck.Type.Type], GHC.Types.Int)

-- | Transformed a parametrized module into an ordinary module where
--   everything is parameterized by the module's parameters. Note that this
--   reuses the names from the original parameterized module.
module Cryptol.Transform.AddModParams
addModParams :: Module -> Either [Name] Module
instance Cryptol.Transform.AddModParams.Inst a => Cryptol.Transform.AddModParams.Inst [a]
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Expr
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Match
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.Decl
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.Type
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.TySyn
instance Cryptol.Transform.AddModParams.Inst Cryptol.TypeCheck.Type.Newtype
instance Cryptol.Transform.AddModParams.AddParams a => Cryptol.Transform.AddModParams.AddParams [a]
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Schema
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Type
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.Expr
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.AST.Decl
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.TySyn
instance Cryptol.Transform.AddModParams.AddParams Cryptol.TypeCheck.Type.Newtype

module Cryptol.ModuleSystem.Interface

-- | The resulting interface generated by a module that has been
--   typechecked.
data Iface
Iface :: !ModName -> IfaceDecls -> IfaceDecls -> IfaceParams -> Iface

-- | Module name
[ifModName] :: Iface -> !ModName

-- | Exported definitions
[ifPublic] :: Iface -> IfaceDecls

-- | Private defintiions
[ifPrivate] :: Iface -> IfaceDecls

-- | Uninterpreted constants (aka module params)
[ifParams] :: Iface -> IfaceParams
data IfaceDecls
IfaceDecls :: Map Name IfaceTySyn -> Map Name IfaceNewtype -> Map Name IfaceAbstractType -> Map Name IfaceDecl -> IfaceDecls
[ifTySyns] :: IfaceDecls -> Map Name IfaceTySyn
[ifNewtypes] :: IfaceDecls -> Map Name IfaceNewtype
[ifAbstractTypes] :: IfaceDecls -> Map Name IfaceAbstractType
[ifDecls] :: IfaceDecls -> Map Name IfaceDecl
type IfaceTySyn = TySyn
ifTySynName :: TySyn -> Name
type IfaceNewtype = Newtype
data IfaceDecl
IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl

-- | Name of thing
[ifDeclName] :: IfaceDecl -> !Name

-- | Type
[ifDeclSig] :: IfaceDecl -> Schema

-- | Pragmas
[ifDeclPragmas] :: IfaceDecl -> [Pragma]

-- | Is this an infix thing
[ifDeclInfix] :: IfaceDecl -> Bool

-- | Fixity information
[ifDeclFixity] :: IfaceDecl -> Maybe Fixity

-- | Documentation
[ifDeclDoc] :: IfaceDecl -> Maybe String
mkIfaceDecl :: Decl -> IfaceDecl
data IfaceParams
IfaceParams :: Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> IfaceParams
[ifParamTypes] :: IfaceParams -> Map Name ModTParam

-- | Constraints on param. types
[ifParamConstraints] :: IfaceParams -> [Located Prop]
[ifParamFuns] :: IfaceParams -> Map Name ModVParam

-- | Generate an Iface from a typechecked module.
genIface :: Module -> Iface

-- | Produce a PrimMap from an interface.
--   
--   NOTE: the map will expose both public and private names.
ifacePrimMap :: Iface -> PrimMap
noIfaceParams :: IfaceParams
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.Iface
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.Iface
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.Iface
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecls
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecl
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecl
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecl
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceParams
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceParams
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceParams
instance GHC.Base.Semigroup Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Base.Monoid Cryptol.ModuleSystem.Interface.IfaceDecls

module Cryptol.ModuleSystem.NamingEnv
data NamingEnv
NamingEnv :: !Map PName [Name] -> !Map PName [Name] -> NamingEnv

-- | Expr renaming environment
[neExprs] :: NamingEnv -> !Map PName [Name]

-- | Type renaming environment
[neTypes] :: NamingEnv -> !Map PName [Name]

-- | Return a list of value-level names to which this parsed name may
--   refer.
lookupValNames :: PName -> NamingEnv -> [Name]

-- | Return a list of type-level names to which this parsed name may refer.
lookupTypeNames :: PName -> NamingEnv -> [Name]

-- | Merge two name maps, collapsing cases where the entries are the same,
--   and producing conflicts otherwise.
merge :: [Name] -> [Name] -> [Name]

-- | Generate a mapping from Ident to Name for a given naming
--   environment.
toPrimMap :: NamingEnv -> PrimMap

-- | Generate a display format based on a naming environment.
toNameDisp :: NamingEnv -> NameDisp

-- | Produce sets of visible names for types and declarations.
--   
--   NOTE: if entries in the NamingEnv would have produced a name clash,
--   they will be omitted from the resulting sets.
visibleNames :: NamingEnv -> (Set Name, Set Name)

-- | Qualify all symbols in a NamingEnv with the given prefix.
qualify :: ModName -> NamingEnv -> NamingEnv
filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv

-- | Singleton type renaming environment.
singletonT :: PName -> Name -> NamingEnv

-- | Singleton expression renaming environment.
singletonE :: PName -> Name -> NamingEnv

-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv
data InModule a
InModule :: !ModName -> a -> InModule a

-- | Generate a NamingEnv using an explicit supply.
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply)
newTop :: FreshM m => ModName -> PName -> Maybe Fixity -> Range -> m Name
newLocal :: FreshM m => PName -> Range -> m Name
newtype BuildNamingEnv
BuildNamingEnv :: SupplyT Id NamingEnv -> BuildNamingEnv
[runBuild] :: BuildNamingEnv -> SupplyT Id NamingEnv

-- | Things that define exported names.
class BindsNames a
namingEnv :: BindsNames a => a -> BuildNamingEnv

-- | Interpret an import in the context of an interface, to produce a name
--   environment for the renamer, and a NameDisp for
--   pretty-printing.
interpImport :: Import -> IfaceDecls -> NamingEnv

-- | Generate a naming environment from a declaration interface, where none
--   of the names are qualified.
unqualifiedEnv :: IfaceDecls -> NamingEnv

-- | Compute an unqualified naming environment, containing the various
--   module parameters.
modParamsNamingEnv :: IfaceParams -> NamingEnv
data ImportIface
ImportIface :: Import -> Iface -> ImportIface
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.ModuleSystem.NamingEnv.InModule a)
instance Data.Foldable.Foldable Cryptol.ModuleSystem.NamingEnv.InModule
instance Data.Traversable.Traversable Cryptol.ModuleSystem.NamingEnv.InModule
instance GHC.Base.Functor Cryptol.ModuleSystem.NamingEnv.InModule
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Generics.Generic Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.ImportIface
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames (GHC.Maybe.Maybe a)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames [a]
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Schema Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Bind Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.TParam Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.TopDecl Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.PrimType Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.ParameterFun Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.ParameterType Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Newtype Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName))
instance GHC.Base.Semigroup Cryptol.ModuleSystem.NamingEnv.BuildNamingEnv
instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.BuildNamingEnv
instance GHC.Base.Semigroup Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.NamingEnv

module Cryptol.ModuleSystem.Renamer
data NamingEnv

-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv

-- | Things that define exported names.
class BindsNames a
namingEnv :: BindsNames a => a -> BuildNamingEnv
data InModule a
InModule :: !ModName -> a -> InModule a

-- | Generate a NamingEnv using an explicit supply.
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply)

-- | Throw errors for any names that overlap in a rewrite environment.
checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning])

-- | Shadow the current naming environment with some more names.
shadowNames :: BindsNames env => env -> RenameM a -> RenameM a
class Rename f
rename :: Rename f => f PName -> RenameM (f Name)
runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a -> (Either [RenamerError] (a, Supply), [RenamerWarning])
data RenameM a
data RenamerError

-- | Multiple imported symbols contain this name
MultipleSyms :: Located PName -> [Name] -> NameDisp -> RenamerError

-- | Expression name is not bound to any definition
UnboundExpr :: Located PName -> NameDisp -> RenamerError

-- | Type name is not bound to any definition
UnboundType :: Located PName -> NameDisp -> RenamerError

-- | An environment has produced multiple overlapping symbols
OverlappingSyms :: [Name] -> NameDisp -> RenamerError

-- | When a value is expected from the naming environment, but one or more
--   types exist instead.
ExpectedValue :: Located PName -> NameDisp -> RenamerError

-- | When a type is missing from the naming environment, but one or more
--   values exist with the same name.
ExpectedType :: Located PName -> NameDisp -> RenamerError

-- | When the fixity of two operators conflict
FixityError :: Located Name -> Fixity -> Located Name -> Fixity -> NameDisp -> RenamerError

-- | When it's not possible to produce a Prop from a Type.
InvalidConstraint :: Type PName -> NameDisp -> RenamerError

-- | When a builtin type/type-function is used incorrectly.
MalformedBuiltin :: Type PName -> PName -> NameDisp -> RenamerError

-- | When a builtin type is named in a binder.
BoundReservedType :: PName -> Maybe Range -> Doc -> NameDisp -> RenamerError

-- | When record updates overlap (e.g., { r | x = e1, x.y = e2 })
OverlappingRecordUpdate :: Located [Selector] -> Located [Selector] -> NameDisp -> RenamerError
data RenamerWarning
SymbolShadowed :: Name -> [Name] -> NameDisp -> RenamerWarning
UnusedName :: Name -> NameDisp -> RenamerWarning
renameVar :: PName -> RenameM Name
renameType :: PName -> RenameM Name
renameModule :: Module PName -> RenameM (NamingEnv, Module Name)
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.EnvCheck
instance GHC.Classes.Eq Cryptol.ModuleSystem.Renamer.EnvCheck
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerWarning
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerError
instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerError
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerError
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TopDecl
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.PrimType
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.ParameterType
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.ParameterFun
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Decl
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Newtype
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Schema
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TParam
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Prop
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Type
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Bind
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.BindDef
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pattern
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.UpdField
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Expr
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TypeInst
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Match
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TySyn
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.PropSyn
instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Cryptol.ModuleSystem.Renamer.RenameM a)
instance (GHC.Base.Semigroup a, GHC.Base.Monoid a) => GHC.Base.Monoid (Cryptol.ModuleSystem.Renamer.RenameM a)
instance GHC.Base.Functor Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Applicative Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Monad Cryptol.ModuleSystem.Renamer.RenameM
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.ModuleSystem.Renamer.RenameM
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerWarning
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerError

module Cryptol.Eval.Monad

-- | The monad for Cryptol evaluation.
data Eval a
Ready :: !a -> Eval a
Thunk :: !EvalOpts -> IO a -> Eval a

-- | Execute the given evaluation action.
runEval :: EvalOpts -> Eval a -> IO a

-- | Some options for evalutaion
data EvalOpts
EvalOpts :: Logger -> PPOpts -> EvalOpts

-- | Where to print stuff (e.g., for trace)
[evalLogger] :: EvalOpts -> Logger

-- | How to pretty print things.
[evalPPOpts] :: EvalOpts -> PPOpts

-- | Access the evaluation options.
getEvalOpts :: Eval EvalOpts

-- | How to pretty print things when evaluating
data PPOpts
PPOpts :: Bool -> Int -> Int -> PPOpts
[useAscii] :: PPOpts -> Bool
[useBase] :: PPOpts -> Int
[useInfLength] :: PPOpts -> Int

-- | Lift an IO computation into the Eval monad.
io :: IO a -> Eval a

-- | Delay the given evaluation computation, returning a thunk which will
--   run the computation when forced. Raise a loop error if the resulting
--   thunk is forced during its own evaluation.
delay :: Maybe String -> Eval a -> Eval (Eval a)

-- | Delay the given evaluation computation, returning a thunk which will
--   run the computation when forced. Run the retry computation
--   instead if the resulting thunk is forced during its own evaluation.
delayFill :: Eval a -> Eval a -> Eval (Eval a)

-- | A computation that returns an already-evaluated value.
ready :: a -> Eval a

-- | Produce a thunk value which can be filled with its associated
--   computation after the fact. A preallocated thunk is returned, along
--   with an operation to fill the thunk with the associated computation.
--   This is used to implement recursive declaration groups.
blackhole :: String -> Eval (Eval a, Eval a -> Eval ())

-- | Data type describing errors that can occur during evaluation.
data EvalError

-- | Out-of-bounds index
InvalidIndex :: Integer -> EvalError

-- | Non-numeric type passed to number function
TypeCannotBeDemoted :: Type -> EvalError

-- | Division or modulus by 0
DivideByZero :: EvalError

-- | Exponentiation by negative integer
NegativeExponent :: EvalError

-- | Logarithm of a negative integer
LogNegative :: EvalError

-- | Bitvector too large
WordTooWide :: Integer -> EvalError

-- | Call to the Cryptol error primitive
UserError :: String -> EvalError

-- | Detectable nontermination
LoopError :: String -> EvalError

-- | Primitive with no implementation
NoPrim :: Name -> EvalError

-- | Panic from an Eval context.
evalPanic :: HasCallStack => String -> [String] -> a

-- | For things like `(inf)</tt> or <tt>`(0-1).
typeCannotBeDemoted :: Type -> a

-- | For division by 0.
divideByZero :: Eval a

-- | For exponentiation by a negative integer.
negativeExponent :: Eval a

-- | For logarithm of a negative integer.
logNegative :: Eval a

-- | For when we know that a word is too wide and will exceed gmp's limits
--   (though words approaching this size will probably cause the system to
--   crash anyway due to lack of memory).
wordTooWide :: Integer -> a

-- | For the Cryptol error function.
cryUserError :: String -> Eval a

-- | For cases where we can detect tight loops.
cryLoopError :: String -> Eval a
cryNoPrimError :: Name -> Eval a

-- | A sequencing operation has gotten an invalid index.
invalidIndex :: Integer -> Eval a
instance GHC.Show.Show Cryptol.Eval.Monad.EvalError
instance Cryptol.Utils.PP.PP Cryptol.Eval.Monad.EvalError
instance GHC.Exception.Type.Exception Cryptol.Eval.Monad.EvalError
instance GHC.Base.Functor Cryptol.Eval.Monad.Eval
instance GHC.Base.Applicative Cryptol.Eval.Monad.Eval
instance GHC.Base.Monad Cryptol.Eval.Monad.Eval
instance Control.Monad.Fail.MonadFail Cryptol.Eval.Monad.Eval
instance Control.Monad.IO.Class.MonadIO Cryptol.Eval.Monad.Eval
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Eval.Monad.Eval a)
instance Control.Monad.Fix.MonadFix Cryptol.Eval.Monad.Eval

module Cryptol.Eval.Type

-- | An evaluated type of kind *. These types do not contain type
--   variables, type synonyms, or type functions.
data TValue

-- | 
--   Bit
--   
TVBit :: TValue

-- | 
--   Integer
--   
TVInteger :: TValue

-- | 
--   Z n
--   
TVIntMod :: Integer -> TValue

-- | 
--   [n]a
--   
TVSeq :: Integer -> TValue -> TValue

-- | 
--   [inf]t
--   
TVStream :: TValue -> TValue

-- | 
--   (a, b, c )
--   
TVTuple :: [TValue] -> TValue

-- | 
--   { x : a, y : b, z : c }
--   
TVRec :: [(Ident, TValue)] -> TValue

-- | 
--   a -> b
--   
TVFun :: TValue -> TValue -> TValue

-- | an abstract type
TVAbstract :: UserTC -> [Either Nat' TValue] -> TValue

-- | Convert a type value back into a regular type
tValTy :: TValue -> Type

-- | True if the evaluated value is Bit
isTBit :: TValue -> Bool

-- | Produce a sequence type value
tvSeq :: Nat' -> TValue -> TValue

-- | Coerce an extended natural into an integer, for values known to be
--   finite
finNat' :: Nat' -> Integer
type TypeEnv = Map TVar (Either Nat' TValue)

-- | Evaluation for types (kind * or #).
evalType :: HasCallStack => TypeEnv -> Type -> Either Nat' TValue

-- | Evaluation for value types (kind *).
evalValType :: HasCallStack => TypeEnv -> Type -> TValue

-- | Evaluation for number types (kind #).
evalNumType :: HasCallStack => TypeEnv -> Type -> Nat'

-- | Reduce type functions, raising an exception for undefined values.
evalTF :: HasCallStack => TFun -> [Nat'] -> Nat'
instance Control.DeepSeq.NFData Cryptol.Eval.Type.TValue
instance GHC.Generics.Generic Cryptol.Eval.Type.TValue
instance GHC.Show.Show Cryptol.Eval.Type.TValue

module Cryptol.Eval.Value

-- | Concrete bitvector values: width, value Invariant: The value must be
--   within the range 0 .. 2^width-1
data BV
BV :: !Integer -> !Integer -> BV

-- | Apply an integer function to the values of bitvectors. This function
--   assumes both bitvectors are the same width.
binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV

-- | Apply an integer function to the values of a bitvector. This function
--   assumes the function will not require masking.
unaryBV :: (Integer -> Integer) -> BV -> BV
bvVal :: BV -> Integer

-- | Smart constructor for BVs that checks for the width limit
mkBv :: Integer -> Integer -> BV

-- | A sequence map represents a mapping from nonnegative integer indices
--   to values. These are used to represent both finite and infinite
--   sequences.
data SeqMap b w i
IndexSeqMap :: !Integer -> Eval (GenValue b w i) -> SeqMap b w i
UpdateSeqMap :: !Map Integer (Eval (GenValue b w i)) -> !Integer -> Eval (GenValue b w i) -> SeqMap b w i
lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)
type SeqValMap = SeqMap Bool BV Integer

-- | Generate a finite sequence map from a list of values
finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i

-- | Generate an infinite sequence map from a stream of values
infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)

-- | Create a finite list of length n of the values from [0..n-1]
--   in the given the sequence emap.
enumerateSeqMap :: Integral n => n -> SeqMap b w i -> [Eval (GenValue b w i)]

-- | Create an infinite stream of all the values in a sequence map
streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]

-- | Reverse the order of a finite sequence map
reverseSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i

-- | Concatenate the first n values of the first sequence map onto
--   the beginning of the second sequence map.
concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i

-- | Given a number n and a sequence map, return two new sequence
--   maps: the first containing the values from `[0..n-1]` and the next
--   containing the values from n onward.
splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)

-- | Drop the first n elements of the given SeqMap.
dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i

-- | Given a sequence map, return a new sequence map that is memoized using
--   a finite map memo table.
memoMap :: SeqMap b w i -> Eval (SeqMap b w i)

-- | Apply the given evaluation function pointwise to the two given
--   sequence maps.
zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> SeqMap b w i -> Eval (SeqMap b w i)

-- | Apply the given function to each value in the given sequence map
mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> Eval (SeqMap b w i)

-- | For efficiency reasons, we handle finite sequences of bits as special
--   cases in the evaluator. In cases where we know it is safe to do so, we
--   prefer to used a "packed word" representation of bit sequences. This
--   allows us to rely directly on Integer types (in the concrete
--   evaluator) and SBV's Word types (in the symbolic simulator).
--   
--   However, if we cannot be sure all the bits of the sequence will
--   eventually be forced, we must instead rely on an explicit sequence of
--   bits representation.
data WordValue b w i

-- | Packed word representation for bit sequences.
WordVal :: !w -> WordValue b w i

-- | Sequence of thunks representing bits.
BitsVal :: !Seq (Eval b) -> WordValue b w i

-- | A large bitvector sequence, represented as a SeqMap of bits.
LargeBitsVal :: !Integer -> !SeqMap b w i -> WordValue b w i

-- | An arbitrarily-chosen number of elements where we switch from a dense
--   sequence representation of bit-level words to SeqMap
--   representation.
largeBitSize :: Integer

-- | Force a word value into packed word form
asWordVal :: BitWord b w i => WordValue b w i -> Eval w

-- | Force a word value into a sequence of bits
asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i

-- | Turn a word value into a sequence of bits, forcing each bit. The
--   sequence is returned in big-endian order.
enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b]

-- | Turn a word value into a sequence of bits, forcing each bit. The
--   sequence is returned in reverse of the usual order, which is
--   little-endian order.
enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b]

-- | Compute the size of a word value
wordValueSize :: BitWord b w i => WordValue b w i -> Integer
checkedSeqIndex :: Seq a -> Integer -> Eval a
checkedIndex :: [a] -> Integer -> Eval a

-- | Select an individual bit from a word value
indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b

-- | Produce a new WordValue from the one given by updating the
--   ith bit with the given bit value.
updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)

-- | Generic value type, parameterized by bit and word types.
--   
--   NOTE: we maintain an important invariant regarding sequence types.
--   VSeq must never be used for finite sequences of bits. Always
--   use the VWord constructor instead! Infinite sequences of bits
--   are handled by the VStream constructor, just as for other
--   types.
data GenValue b w i

-- | 
--   { .. }
--   
VRecord :: ![(Ident, Eval (GenValue b w i))] -> GenValue b w i

-- | 
--   ( .. )
--   
VTuple :: ![Eval (GenValue b w i)] -> GenValue b w i

-- | 
--   Bit
--   
VBit :: !b -> GenValue b w i

-- |  Integer  or  Z n 
VInteger :: !i -> GenValue b w i

-- |  [n]a  Invariant: VSeq is never a sequence of bits
VSeq :: !Integer -> !SeqMap b w i -> GenValue b w i

-- | 
--   [n]Bit
--   
VWord :: !Integer -> !Eval (WordValue b w i) -> GenValue b w i

-- | 
--   [inf]a
--   
VStream :: !SeqMap b w i -> GenValue b w i

-- | functions
VFun :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i

-- | polymorphic values (kind *)
VPoly :: (TValue -> Eval (GenValue b w i)) -> GenValue b w i

-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Eval (GenValue b w i)) -> GenValue b w i

-- | Force the evaluation of a word value
forceWordValue :: WordValue b w i -> Eval ()

-- | Force the evaluation of a value
forceValue :: GenValue b w i -> Eval ()
type Value = GenValue Bool BV Integer
defaultPPOpts :: PPOpts
atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
ppValue :: forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
asciiMode :: PPOpts -> Integer -> Bool
integerToChar :: Integer -> Char
ppBV :: PPOpts -> BV -> Doc

-- | This type class defines a collection of operations on bits and words
--   that are necessary to define generic evaluator primitives that operate
--   on both concrete and symbolic values uniformly.
class BitWord b w i | b -> w, w -> i, i -> b

-- | Pretty-print an individual bit
ppBit :: BitWord b w i => b -> Doc

-- | Pretty-print a word value
ppWord :: BitWord b w i => PPOpts -> w -> Doc

-- | Pretty-print an integer value
ppInteger :: BitWord b w i => PPOpts -> i -> Doc

-- | Attempt to render a word value as an ASCII character. Return
--   Nothing if the character value is unknown (e.g., for symbolic
--   values).
wordAsChar :: BitWord b w i => w -> Maybe Char

-- | The number of bits in a word value.
wordLen :: BitWord b w i => w -> Integer

-- | Construct a literal bit value from a boolean.
bitLit :: BitWord b w i => Bool -> b

-- | Construct a literal word value given a bit width and a value.
wordLit :: BitWord b w i => Integer -> Integer -> w

-- | Construct a literal integer value from the given integer.
integerLit :: BitWord b w i => Integer -> i

-- | Extract the numbered bit from the word.
--   
--   NOTE: this assumes that the sequence of bits is big-endian and finite,
--   so the bit numbered 0 is the most significant bit.
wordBit :: BitWord b w i => w -> Integer -> b

-- | Update the numbered bit in the word.
--   
--   NOTE: this assumes that the sequence of bits is big-endian and finite,
--   so the bit numbered 0 is the most significant bit.
wordUpdate :: BitWord b w i => w -> Integer -> b -> w

-- | Construct a word value from a finite sequence of bits. NOTE: this
--   assumes that the sequence of bits is big-endian and finite, so the
--   first element of the list will be the most significant bit.
packWord :: BitWord b w i => [b] -> w

-- | Deconstruct a packed word value in to a finite sequence of bits. NOTE:
--   this produces a list of bits that represent a big-endian word, so the
--   most significant bit is the first element of the list.
unpackWord :: BitWord b w i => w -> [b]

-- | Concatenate the two given word values. NOTE: the first argument
--   represents the more-significant bits
joinWord :: BitWord b w i => w -> w -> w

-- | Take the most-significant bits, and return those bits and the
--   remainder. The first element of the pair is the most significant bits.
--   The two integer sizes must sum to the length of the given word value.
splitWord :: BitWord b w i => Integer -> Integer -> w -> (w, w)

-- | Extract a subsequence of bits from a packed word value. The first
--   integer argument is the number of bits in the resulting word. The
--   second integer argument is the number of less-significant digits to
--   discard. Stated another way, the operation `extractWord n i w` is
--   equivalent to first shifting w right by i bits, and
--   then truncating to n bits.
extractWord :: BitWord b w i => Integer -> Integer -> w -> w

-- | 2's complement addition of packed words. The arguments must have equal
--   bit width, and the result is of the same width. Overflow is silently
--   discarded.
wordPlus :: BitWord b w i => w -> w -> w

-- | 2's complement subtraction of packed words. The arguments must have
--   equal bit width, and the result is of the same width. Overflow is
--   silently discarded.
wordMinus :: BitWord b w i => w -> w -> w

-- | 2's complement multiplication of packed words. The arguments must have
--   equal bit width, and the result is of the same width. The high bits of
--   the multiplication are silently discarded.
wordMult :: BitWord b w i => w -> w -> w

-- | Construct an integer value from the given packed word.
wordToInt :: BitWord b w i => w -> i

-- | Addition of unbounded integers.
intPlus :: BitWord b w i => i -> i -> i

-- | Subtraction of unbounded integers.
intMinus :: BitWord b w i => i -> i -> i

-- | Multiplication of unbounded integers.
intMult :: BitWord b w i => i -> i -> i

-- | Addition of integers modulo n, for a concrete positive integer n.
intModPlus :: BitWord b w i => Integer -> i -> i -> i

-- | Subtraction of integers modulo n, for a concrete positive integer n.
intModMinus :: BitWord b w i => Integer -> i -> i -> i

-- | Multiplication of integers modulo n, for a concrete positive integer
--   n.
intModMult :: BitWord b w i => Integer -> i -> i -> i

-- | Construct a packed word of the specified width from an integer value.
wordFromInt :: BitWord b w i => Integer -> i -> w

-- | This class defines additional operations necessary to define generic
--   evaluation functions.
class BitWord b w i => EvalPrims b w i

-- | Eval prim binds primitive declarations to the primitive values that
--   implement them. Returns Nothing for abstract primitives (i.e.,
--   once that are not implemented by this backend).
evalPrim :: EvalPrims b w i => Decl -> Maybe (GenValue b w i)

-- | ifthenelse operation. Choose either the 'then' value or the
--   'else' value depending on the value of the test bit.
iteValue :: EvalPrims b w i => b -> Eval (GenValue b w i) -> Eval (GenValue b w i) -> Eval (GenValue b w i)
mask :: Integer -> Integer -> Integer

-- | Create a packed word of n bits.
word :: BitWord b w i => Integer -> Integer -> GenValue b w i
lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i

-- | Functions that assume word inputs
wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i

-- | A type lambda that expects a Type.
tlam :: (TValue -> GenValue b w i) -> GenValue b w i

-- | A type lambda that expects a Type of kind #.
nlam :: (Nat' -> GenValue b w i) -> GenValue b w i

-- | Generate a stream.
toStream :: [GenValue b w i] -> Eval (GenValue b w i)
toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i

-- | This is strict!
boolToWord :: [Bool] -> Value

-- | Construct either a finite sequence, or a stream. In the finite case,
--   record whether or not the elements were bits, to aid pretty-printing.
toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)

-- | Construct either a finite sequence, or a stream. In the finite case,
--   record whether or not the elements were bits, to aid pretty-printing.
mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i

-- | Extract a bit value.
fromVBit :: GenValue b w i -> b

-- | Extract an integer value.
fromVInteger :: GenValue b w i -> i

-- | Extract a finite sequence value.
fromVSeq :: GenValue b w i -> SeqMap b w i

-- | Extract a sequence.
fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
fromStr :: Value -> Eval String
fromBit :: GenValue b w i -> Eval b
fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)

-- | Extract a packed word.
fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer

-- | If the given list of values are all fully-evaluated thunks containing
--   bits, return a packed word built from the same bits. However, if any
--   value is not a fully-evaluated bit, return Nothing.
tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w

-- | Turn a value into an integer represented by w bits.
fromWord :: String -> Value -> Eval Integer

-- | Extract a function from a value.
fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)

-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)

-- | Extract a polymorphic function from a value.
fromVNumPoly :: GenValue b w i -> Nat' -> Eval (GenValue b w i)

-- | Extract a tuple from a value.
fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]

-- | Extract a record from a value.
fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]

-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)

-- | Given an expected type, returns an expression that evaluates to this
--   value, if we can determine it.
--   
--   XXX: View patterns would probably clean up this definition a lot.
toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
instance (Control.DeepSeq.NFData w, Control.DeepSeq.NFData b) => Control.DeepSeq.NFData (Cryptol.Eval.Value.WordValue b w i)
instance GHC.Generics.Generic (Cryptol.Eval.Value.WordValue b w i)
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData i, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Value.GenValue b w i)
instance GHC.Generics.Generic (Cryptol.Eval.Value.GenValue b w i)
instance Control.DeepSeq.NFData Cryptol.Eval.Value.BV
instance GHC.Generics.Generic Cryptol.Eval.Value.BV
instance Cryptol.Eval.Value.BitWord GHC.Types.Bool Cryptol.Eval.Value.BV GHC.Integer.Type.Integer
instance Control.DeepSeq.NFData (Cryptol.Eval.Value.SeqMap b w i)
instance (GHC.Show.Show b, GHC.Show.Show w, GHC.Show.Show i) => GHC.Show.Show (Cryptol.Eval.Value.GenValue b w i)
instance GHC.Show.Show Cryptol.Eval.Value.BV

module Cryptol.Testing.Concrete

-- | A test result is either a pass, a failure due to evaluating to
--   False, or a failure due to an exception raised during
--   evaluation
data TestResult
Pass :: TestResult
FailFalse :: [Value] -> TestResult
FailError :: EvalError -> [Value] -> TestResult
isPass :: TestResult -> Bool

-- | Apply a testable value to some arguments. Note that this function
--   assumes that the values come from a call to testableType (i.e.,
--   things are type-correct). We run in the IO monad in order to catch any
--   EvalErrors.
runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult

-- | Given a (function) type, compute all possible inputs for it. We also
--   return the types of the arguments and the total number of test (i.e.,
--   the length of the outer list.
testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])

-- | Given a fully-evaluated type, try to compute the number of values in
--   it. Returns Nothing for infinite types, user-defined types,
--   polymorphic types, and, currently, function spaces. Of course, we can
--   easily compute the sizes of function spaces, but we can't easily
--   enumerate their inhabitants.
typeSize :: Type -> Maybe Integer

-- | Returns all the values in a type. Returns an empty list of values, for
--   types where typeSize returned Nothing.
typeValues :: Type -> [Value]
data TestSpec m s
TestSpec :: (Integer -> s -> m (TestResult, s)) -> String -> Integer -> Maybe Integer -> (Integer -> Integer -> m ()) -> m () -> (TestResult -> m ()) -> m () -> TestSpec m s
[testFn] :: TestSpec m s -> Integer -> s -> m (TestResult, s)

-- | The property as entered by the user
[testProp] :: TestSpec m s -> String
[testTotal] :: TestSpec m s -> Integer

-- | Nothing indicates infinity
[testPossible] :: TestSpec m s -> Maybe Integer
[testRptProgress] :: TestSpec m s -> Integer -> Integer -> m ()
[testClrProgress] :: TestSpec m s -> m ()
[testRptFailure] :: TestSpec m s -> TestResult -> m ()
[testRptSuccess] :: TestSpec m s -> m ()
data TestReport
TestReport :: TestResult -> String -> Integer -> Maybe Integer -> TestReport
[reportResult] :: TestReport -> TestResult

-- | The property as entered by the user
[reportProp] :: TestReport -> String
[reportTestsRun] :: TestReport -> Integer
[reportTestsPossible] :: TestReport -> Maybe Integer
runTests :: Monad m => TestSpec m s -> s -> m TestReport

module Cryptol.Symbolic.Value
type SBool = SVal
type SWord = SVal
type SInteger = SVal
literalSWord :: Int -> Integer -> SWord
fromBitsLE :: [SBool] -> SWord
forallBV_ :: Int -> Symbolic SWord
existsBV_ :: Int -> Symbolic SWord
forallSBool_ :: Symbolic SBool
existsSBool_ :: Symbolic SBool
forallSInteger_ :: Symbolic SBool
existsSInteger_ :: Symbolic SBool
type Value = GenValue SBool SWord SInteger

-- | An evaluated type of kind *. These types do not contain type
--   variables, type synonyms, or type functions.
data TValue

-- | True if the evaluated value is Bit
isTBit :: TValue -> Bool

-- | Produce a sequence type value
tvSeq :: Nat' -> TValue -> TValue

-- | Generic value type, parameterized by bit and word types.
--   
--   NOTE: we maintain an important invariant regarding sequence types.
--   VSeq must never be used for finite sequences of bits. Always
--   use the VWord constructor instead! Infinite sequences of bits
--   are handled by the VStream constructor, just as for other
--   types.
data GenValue b w i

-- | 
--   { .. }
--   
VRecord :: ![(Ident, Eval (GenValue b w i))] -> GenValue b w i

-- | 
--   ( .. )
--   
VTuple :: ![Eval (GenValue b w i)] -> GenValue b w i

-- | 
--   Bit
--   
VBit :: !b -> GenValue b w i

-- |  Integer  or  Z n 
VInteger :: !i -> GenValue b w i

-- |  [n]a  Invariant: VSeq is never a sequence of bits
VSeq :: !Integer -> !SeqMap b w i -> GenValue b w i

-- | 
--   [n]Bit
--   
VWord :: !Integer -> !Eval (WordValue b w i) -> GenValue b w i

-- | 
--   [inf]a
--   
VStream :: !SeqMap b w i -> GenValue b w i

-- | functions
VFun :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i

-- | polymorphic values (kind *)
VPoly :: (TValue -> Eval (GenValue b w i)) -> GenValue b w i

-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i

-- | A type lambda that expects a Type.
tlam :: (TValue -> GenValue b w i) -> GenValue b w i

-- | Generate a stream.
toStream :: [GenValue b w i] -> Eval (GenValue b w i)
toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i

-- | Construct either a finite sequence, or a stream. In the finite case,
--   record whether or not the elements were bits, to aid pretty-printing.
toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)

-- | Extract a bit value.
fromVBit :: GenValue b w i -> b

-- | Extract a function from a value.
fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)

-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)

-- | Extract a tuple from a value.
fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]

-- | Extract a record from a value.
fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]

-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)

-- | Extract a sequence.
fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)

-- | Extract a packed word.
fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
evalPanic :: String -> [String] -> a
iteSValue :: SBool -> Value -> Value -> Eval Value
mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger
mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
instance Cryptol.Eval.Value.BitWord Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord Cryptol.Symbolic.Value.SInteger

module Cryptol.Eval.Env
data GenEvalEnv b w i
EvalEnv :: !Map Name (Eval (GenValue b w i)) -> !TypeEnv -> GenEvalEnv b w i
[envVars] :: GenEvalEnv b w i -> !Map Name (Eval (GenValue b w i))
[envTypes] :: GenEvalEnv b w i -> !TypeEnv
ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc

-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv b w i

-- | Bind a variable in the evaluation environment.
bindVar :: Name -> Eval (GenValue b w i) -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)

-- | Bind a variable to a value in the evaluation environment, without
--   creating a thunk.
bindVarDirect :: Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i

-- | Lookup a variable in the environment.
lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))

-- | Bind a type variable of kind *.
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i

-- | Lookup a type variable.
lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue)
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData i, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Env.GenEvalEnv b w i)
instance GHC.Generics.Generic (Cryptol.Eval.Env.GenEvalEnv b w i)
instance GHC.Base.Semigroup (Cryptol.Eval.Env.GenEvalEnv b w i)
instance GHC.Base.Monoid (Cryptol.Eval.Env.GenEvalEnv b w i)

module Cryptol.Eval

-- | Extend the given evaluation environment with all the declarations
--   contained in the given module.
moduleEnv :: EvalPrims b w i => Module -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)

-- | Execute the given evaluation action.
runEval :: EvalOpts -> Eval a -> IO a

-- | Some options for evalutaion
data EvalOpts
EvalOpts :: Logger -> PPOpts -> EvalOpts

-- | Where to print stuff (e.g., for trace)
[evalLogger] :: EvalOpts -> Logger

-- | How to pretty print things.
[evalPPOpts] :: EvalOpts -> PPOpts

-- | How to pretty print things when evaluating
data PPOpts
PPOpts :: Bool -> Int -> Int -> PPOpts
[useAscii] :: PPOpts -> Bool
[useBase] :: PPOpts -> Int
[useInfLength] :: PPOpts -> Int
defaultPPOpts :: PPOpts

-- | The monad for Cryptol evaluation.
data Eval a
type EvalEnv = GenEvalEnv Bool BV Integer

-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv b w i

-- | Evaluate a Cryptol expression to a value. This evaluator is
--   parameterized by the EvalPrims class, which defines the
--   behavior of bits and words, in addition to providing implementations
--   for all the primitives.
evalExpr :: EvalPrims b w i => GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)

-- | Extend the given evaluation environment with the result of evaluating
--   the given collection of declaration groups.
evalDecls :: EvalPrims b w i => [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)

-- | Apply the the given "selector" form to the given value. This function
--   pushes tuple and record selections pointwise down into other value
--   constructs (e.g., streams and functions).
evalSel :: forall b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i)
evalSetSel :: forall b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)

-- | Data type describing errors that can occur during evaluation.
data EvalError

-- | Out-of-bounds index
InvalidIndex :: Integer -> EvalError

-- | Non-numeric type passed to number function
TypeCannotBeDemoted :: Type -> EvalError

-- | Division or modulus by 0
DivideByZero :: EvalError

-- | Exponentiation by negative integer
NegativeExponent :: EvalError

-- | Logarithm of a negative integer
LogNegative :: EvalError

-- | Bitvector too large
WordTooWide :: Integer -> EvalError

-- | Call to the Cryptol error primitive
UserError :: String -> EvalError

-- | Detectable nontermination
LoopError :: String -> EvalError

-- | Primitive with no implementation
NoPrim :: Name -> EvalError

-- | Force the evaluation of a value
forceValue :: GenValue b w i -> Eval ()
instance GHC.Base.Semigroup (Cryptol.Eval.ListEnv b w i)
instance GHC.Base.Monoid (Cryptol.Eval.ListEnv b w i)

module Cryptol.Utils.Patterns
newtype Match b
Match :: (forall r. r -> (b -> r) -> r) -> Match b
type Pat a b = a -> Match b
(|||) :: Pat a b -> Pat a b -> Pat a b

-- | Check that a value satisfies multiple patterns. For example, an "as"
--   pattern is (__ &&& p).
(&&&) :: Pat a b -> Pat a c -> Pat a (b, c)

-- | Match a value, and modify the result.
(~>) :: Pat a b -> (b -> c) -> Pat a c

-- | Match a value, and return the given result
(~~>) :: Pat a b -> c -> Pat a c

-- | View pattern.
(<~) :: (a -> b) -> Pat b c -> Pat a c

-- | Variable pattern.
__ :: Pat a a

-- | Constant pattern.
succeed :: a -> Pat x a

-- | Predicate pattern
checkThat :: (a -> Bool) -> Pat a ()

-- | Check for exact value.
lit :: Eq a => a -> Pat a ()

-- | Match a pattern, using the given default if valure.
matchDefault :: a -> Match a -> a

-- | Match an irrefutable pattern. Crashes on faliure.
match :: Match a -> a
matchMaybe :: Match a -> Maybe a
list :: [Pat a b] -> Pat [a] [b]
(><) :: Pat a b -> Pat x y -> Pat (a, x) (b, y)
class Matches thing pats res | pats -> thing res
matches :: Matches thing pats res => thing -> pats -> Match res
instance (f GHC.Types.~ Cryptol.Utils.Patterns.Pat a a1', a1 GHC.Types.~ Cryptol.Utils.Patterns.Pat a1' r1) => Cryptol.Utils.Patterns.Matches a (f, a1) r1
instance (op GHC.Types.~ Cryptol.Utils.Patterns.Pat a (a1', a2'), a1 GHC.Types.~ Cryptol.Utils.Patterns.Pat a1' r1, a2 GHC.Types.~ Cryptol.Utils.Patterns.Pat a2' r2) => Cryptol.Utils.Patterns.Matches a (op, a1, a2) (r1, r2)
instance (op GHC.Types.~ Cryptol.Utils.Patterns.Pat a (a1', a2', a3'), a1 GHC.Types.~ Cryptol.Utils.Patterns.Pat a1' r1, a2 GHC.Types.~ Cryptol.Utils.Patterns.Pat a2' r2, a3 GHC.Types.~ Cryptol.Utils.Patterns.Pat a3' r3) => Cryptol.Utils.Patterns.Matches a (op, a1, a2, a3) (r1, r2, r3)
instance GHC.Base.Functor Cryptol.Utils.Patterns.Match
instance GHC.Base.Applicative Cryptol.Utils.Patterns.Match
instance GHC.Base.Monad Cryptol.Utils.Patterns.Match
instance Control.Monad.Fail.MonadFail Cryptol.Utils.Patterns.Match
instance GHC.Base.Alternative Cryptol.Utils.Patterns.Match
instance GHC.Base.MonadPlus Cryptol.Utils.Patterns.Match

module Cryptol.TypeCheck.TypePat
aInf :: Pat Type ()
aNat :: Pat Type Integer
aNat' :: Pat Type Nat'
anAdd :: Pat Type (Type, Type)
(|-|) :: Pat Type (Type, Type)
aMul :: Pat Type (Type, Type)
(|^|) :: Pat Type (Type, Type)
(|/|) :: Pat Type (Type, Type)
(|%|) :: Pat Type (Type, Type)
aMin :: Pat Type (Type, Type)
aMax :: Pat Type (Type, Type)
aWidth :: Pat Type Type
aCeilDiv :: Pat Type (Type, Type)
aCeilMod :: Pat Type (Type, Type)
aLenFromThenTo :: Pat Type (Type, Type, Type)
aLiteral :: Pat Prop (Type, Type)
aLogic :: Pat Prop Type
aTVar :: Pat Type TVar
aFreeTVar :: Pat Type TVar
aBit :: Pat Type ()
aSeq :: Pat Type (Type, Type)
aWord :: Pat Type Type
aChar :: Pat Type ()
aTuple :: Pat Type [Type]
aRec :: Pat Type [(Ident, Type)]
(|->|) :: Pat Type (Type, Type)
aFin :: Pat Prop Type
(|=|) :: Pat Prop (Type, Type)
(|/=|) :: Pat Prop (Type, Type)
(|>=|) :: Pat Prop (Type, Type)
aCmp :: Pat Prop Type
aArith :: Pat Prop Type
aAnd :: Pat Prop (Prop, Prop)
aTrue :: Pat Prop ()
anError :: Kind -> Pat Type TCErrorMessage

module Cryptol.TypeCheck.SimpType
tRebuild' :: Bool -> Type -> Type
tRebuild :: Type -> Type
tCon :: TCon -> [Type] -> Type
tAdd :: Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tMax :: Type -> Type -> Type
tWidth :: Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
total :: ([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
op1 :: (a -> b) -> [a] -> b
op2 :: (a -> a -> b) -> [a] -> b
op3 :: (a -> a -> a -> b) -> [a] -> b

-- | Common checks: check for error, or simple full evaluation.
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type

module Cryptol.TypeCheck.Solver.Utils

-- | All ways to split a type in the form: `a + t1`, where a is a
--   variable.
splitVarSummands :: Type -> [(TVar, Type)]

-- | Check if we can express a type in the form: `a + t1`.
splitVarSummand :: TVar -> Type -> Maybe Type

-- | Check if we can express a type in the form: `k + t1`, where k
--   is a constant > 0. This assumes that the type has been simplified
--   already, so that constants are floated to the left.
splitConstSummand :: Type -> Maybe (Integer, Type)

-- | Check if we can express a type in the form: `k * t1`, where k
--   is a constant > 1 This assumes that the type has been simplified
--   already, so that constants are floated to the left.
splitConstFactor :: Type -> Maybe (Integer, Type)

-- | Solving class constraints.
module Cryptol.TypeCheck.Solver.Class

-- | Solve class constraints. If not, then we return Nothing. If
--   solved, then we return Just a list of sub-goals.
classStep :: Prop -> Solved

-- | Solve a Zero constraint by instance, if possible.
solveZeroInst :: Type -> Solved

-- | Solve a Logic constraint by instance, if possible.
solveLogicInst :: Type -> Solved

-- | Solve an Arith constraint by instance, if possible.
solveArithInst :: Type -> Solved

-- | Solve Cmp constraints.
solveCmpInst :: Type -> Solved

-- | Solve SignedCmp constraints.
solveSignedCmpInst :: Type -> Solved

-- | Solve Literal constraints.
solveLiteralInst :: Type -> Type -> Solved

-- | Add propositions that are implied by the given one. The result
--   contains the orignal proposition, and maybe some more.
expandProp :: Prop -> [Prop]

-- | This module generates random values for Cryptol types.
module Cryptol.Testing.Random
type Gen g b w i = Integer -> g -> (GenValue b w i, g)

-- | Apply a testable value to some randomly-generated arguments. Returns
--   Nothing if the function returned True, or `Just
--   counterexample` if it returned False.
--   
--   Please note that this function assumes that the generators match the
--   supplied value, otherwise we'll panic.
runOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Bool BV Integer] -> Integer -> g -> IO (TestResult, g)
returnOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Bool BV Integer] -> Integer -> g -> IO ([Value], Value, g)

-- | Return a collection of random tests.
returnTests :: RandomGen g => g -> EvalOpts -> [Gen g Bool BV Integer] -> Value -> Int -> IO [([Value], Value)]

-- | Given a (function) type, compute generators for the function's
--   arguments. This is like testableType, but allows the result
--   to be any finite type instead of just Bit.
dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]

-- | Given a (function) type, compute generators for the function's
--   arguments. Currently we do not support polymorphic functions. In
--   principle, we could apply these to random types, and test the results.
testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV Integer]

-- | A generator for values of the given type. This fails if we are given a
--   type that lacks a suitable random value generator.
randomValue :: (BitWord b w i, RandomGen g) => Type -> Maybe (Gen g b w i)

-- | Generate a random bit value.
randomBit :: (BitWord b w i, RandomGen g) => Gen g b w i
randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)

-- | Generate a random integer value. The size parameter is assumed to vary
--   between 1 and 100, and we use it to generate smaller numbers first.
randomInteger :: (BitWord b w i, RandomGen g) => Gen g b w i
randomIntMod :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i

-- | Generate a random word of the given length (i.e., a value of type
--   [w]) The size parameter is assumed to vary between 1 and 100,
--   and we use it to generate smaller numbers first.
randomWord :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i

-- | Generate a random infinite stream value.
randomStream :: RandomGen g => Gen g b w i -> Gen g b w i

-- | Generate a random sequence. This should be used for sequences other
--   than bits. For sequences of bits use "randomWord".
randomSequence :: RandomGen g => Integer -> Gen g b w i -> Gen g b w i

-- | Generate a random tuple value.
randomTuple :: RandomGen g => [Gen g b w i] -> Gen g b w i

-- | Generate a random record value.
randomRecord :: RandomGen g => [(Ident, Gen g b w i)] -> Gen g b w i

module Cryptol.Prims.Eval
primTable :: Map Ident Value

-- | Make a numeric literal value at the given type.
mkLit :: BitWord b w i => TValue -> Integer -> GenValue b w i

-- | Make a numeric constant.
ecNumberV :: BitWord b w i => GenValue b w i

-- | Convert a word to a non-negative integer.
ecToIntegerV :: BitWord b w i => GenValue b w i

-- | Convert an unbounded integer to a packed bitvector.
ecFromIntegerV :: BitWord b w i => (Integer -> i -> i) -> GenValue b w i

-- | Create a packed word
modExp :: Integer -> BV -> BV -> Eval BV
intModExp :: Integer -> Integer -> Integer -> Eval Integer
integerExp :: Integer -> Integer -> Eval Integer
integerLg2 :: Integer -> Eval Integer
integerNeg :: Integer -> Eval Integer
intModNeg :: Integer -> Integer -> Eval Integer
doubleAndAdd :: Integer -> Integer -> Integer -> Integer
type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
binary :: Binary b w i -> GenValue b w i
type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i)
unary :: Unary b w i -> GenValue b w i

-- | Turn a normal binop on Integers into one that can also deal with a
--   bitsize. However, if the bitvector size is 0, always return the 0
--   bitvector.
liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV

-- | Turn a normal binop on Integers into one that can also deal with a
--   bitsize. Generate a thunk that throws a divide by 0 error when forced
--   if the second argument is 0. However, if the bitvector size is 0,
--   always return the 0 bitvector.
liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV
type BinArith w = Integer -> w -> w -> Eval w
liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
liftBinIntMod :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> Eval Integer
liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
modWrap :: Integral a => a -> a -> Eval a
arithBinary :: forall b w i. BitWord b w i => BinArith w -> (i -> i -> Eval i) -> (Integer -> i -> i -> Eval i) -> Binary b w i
type UnaryArith w = Integer -> w -> Eval w
liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV
arithUnary :: forall b w i. BitWord b w i => UnaryArith w -> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i
arithNullary :: forall b w i. BitWord b w i => (Integer -> w) -> i -> (Integer -> i) -> TValue -> GenValue b w i
lg2 :: Integer -> Integer
addV :: BitWord b w i => Binary b w i
subV :: BitWord b w i => Binary b w i
mulV :: BitWord b w i => Binary b w i
intV :: BitWord b w i => i -> TValue -> GenValue b w i
cmpValue :: BitWord b w i => (b -> b -> Eval a -> Eval a) -> (w -> w -> Eval a -> Eval a) -> (i -> i -> Eval a -> Eval a) -> (Integer -> i -> i -> Eval a -> Eval a) -> TValue -> GenValue b w i -> GenValue b w i -> Eval a -> Eval a
lexCompare :: TValue -> Value -> Value -> Eval Ordering
signedLexCompare :: TValue -> Value -> Value -> Eval Ordering

-- | Process two elements based on their lexicographic ordering.
cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer

-- | Process two elements based on their lexicographic ordering, using
--   signed comparisons
signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer

-- | Lifted operation on finite bitsequences. Used for signed comparisons
--   and arithemtic.
liftWord :: BitWord b w i => (w -> w -> Eval (GenValue b w i)) -> GenValue b w i
liftSigned :: (Integer -> Integer -> Integer -> Eval BV) -> BinArith BV
signedBV :: BV -> Integer
signedValue :: Integer -> Integer -> Integer
bvSlt :: Integer -> Integer -> Integer -> Eval Value
bvSdiv :: Integer -> Integer -> Integer -> Eval BV
bvSrem :: Integer -> Integer -> Integer -> Eval BV
sshrV :: Value

-- | Signed carry bit.
scarryV :: Value

-- | Unsigned carry bit.
carryV :: Value
zeroV :: forall b w i. BitWord b w i => TValue -> GenValue b w i
joinWordVal :: BitWord b w i => WordValue b w i -> WordValue b w i -> WordValue b w i
joinWords :: forall b w i. BitWord b w i => Integer -> Integer -> SeqMap b w i -> Eval (GenValue b w i)
joinSeq :: BitWord b w i => Nat' -> Integer -> TValue -> SeqMap b w i -> Eval (GenValue b w i)

-- | Join a sequence of sequences into a single sequence.
joinV :: BitWord b w i => Nat' -> Integer -> TValue -> GenValue b w i -> Eval (GenValue b w i)
splitWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> (WordValue b w i, WordValue b w i)
splitAtV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
extractWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> WordValue b w i

-- | Split implementation.
ecSplitV :: BitWord b w i => GenValue b w i
reverseV :: forall b w i. BitWord b w i => GenValue b w i -> Eval (GenValue b w i)
transposeV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
ccatV :: (Show b, Show w, BitWord b w i) => Nat' -> Nat' -> TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
wordValLogicOp :: BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> WordValue b w i -> WordValue b w i -> Eval (WordValue b w i)

-- | Merge two values given a binop. This is used for and, or and xor.
logicBinary :: forall b w i. BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> Binary b w i
wordValUnaryOp :: BitWord b w i => (b -> b) -> (w -> w) -> WordValue b w i -> Eval (WordValue b w i)
logicUnary :: forall b w i. BitWord b w i => (b -> b) -> (w -> w) -> Unary b w i
logicShift :: (Integer -> Integer -> Integer -> Integer) -> (Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)) -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) -> Value
shiftLW :: Integer -> Integer -> Integer -> Integer
shiftLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftRW :: Integer -> Integer -> Integer -> Integer
shiftRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateLW :: Integer -> Integer -> Integer -> Integer
rotateLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateRW :: Integer -> Integer -> Integer -> Integer
rotateRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap

-- | Indexing operations.
indexPrim :: BitWord b w i => (Maybe Integer -> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i)) -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i)) -> GenValue b w i
indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
updateFront :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer)
updateFront_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer)
updateBack :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer)
updateBack_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer)
updatePrim :: BitWord b w i => (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i)) -> (Nat' -> TValue -> SeqMap b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i)) -> GenValue b w i
fromToV :: BitWord b w i => GenValue b w i
fromThenToV :: BitWord b w i => GenValue b w i
infFromV :: BitWord b w i => GenValue b w i
infFromThenV :: BitWord b w i => GenValue b w i

-- | Produce a random value with the given seed. If we do not support
--   making values of the given type, return zero of that type. TODO: do
--   better than returning zero
randomV :: BitWord b w i => TValue -> Integer -> GenValue b w i
errorV :: forall b w i. BitWord b w i => TValue -> String -> Eval (GenValue b w i)
instance Cryptol.Eval.Value.EvalPrims GHC.Types.Bool Cryptol.Eval.Value.BV GHC.Integer.Type.Integer

module Cryptol.Symbolic.Prims
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
primTable :: Map Ident Value

-- | Barrel-shifter algorithm. Takes a list of bits in big-endian order.
shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a
logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value
indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value
indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value
indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value
indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value

-- | Compare a symbolic word value with a concrete integer.
wordValueEqualsInteger :: WordValue SBool SWord SInteger -> Integer -> Eval SBool
lazyMergeBit :: SBool -> Eval SBool -> Eval SBool -> Eval SBool
updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger)
updateFrontSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger)
updateBackSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
asBitList :: [Eval SBool] -> Maybe [SBool]
asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord]
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
liftBin :: (a -> b -> c) -> a -> b -> Eval c
liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a
sExp :: Integer -> SWord -> SWord -> Eval SWord
sModAdd :: Integer -> SInteger -> SInteger -> Eval SInteger
sModSub :: Integer -> SInteger -> SInteger -> Eval SInteger
sModMult :: Integer -> SInteger -> SInteger -> Eval SInteger
sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger

-- | Ceiling (log_2 x)
sLg2 :: Integer -> SWord -> Eval SWord

-- | Ceiling (log_2 x)
svLg2 :: SInteger -> Eval SInteger
svModLg2 :: Integer -> SInteger -> Eval SInteger
cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpMod :: (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
svDivisible :: Integer -> SInteger -> SBool
cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) -> (SWord -> SWord -> Eval SBool -> Eval SBool) -> (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool) -> SBool -> Binary SBool SWord SInteger
signedQuot :: SWord -> SWord -> SWord
signedRem :: SWord -> SWord -> SWord
sshrV :: Value
carry :: SWord -> SWord -> Eval Value
scarry :: SWord -> SWord -> Eval Value
instance Cryptol.Eval.Value.EvalPrims Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord Cryptol.Symbolic.Value.SInteger

module Cryptol.TypeCheck.Solver.Numeric

-- | Try to solve t1 = t2
cryIsEqual :: Ctxt -> Type -> Type -> Solved

-- | Try to solve t1 /= t2
cryIsNotEqual :: Ctxt -> Type -> Type -> Solved

-- | Try to solve t1 >= t2
cryIsGeq :: Ctxt -> Type -> Type -> Solved

module Cryptol.TypeCheck.SimpleSolver
simplify :: Ctxt -> Prop -> Prop
simplifyStep :: Ctxt -> Prop -> Solved

module Cryptol.TypeCheck.Subst

-- | A Subst value represents a substitution that maps each
--   TVar to a Type.
--   
--   Invariant: If there is a mapping from TVFree _ _ tps _ to a
--   type t, then t must not mention (directly or
--   indirectly) any type parameter that is not in tps. In
--   particular, if t contains a variable TVFree _ _ tps2
--   _, then tps2 must be a subset of tps. This
--   ensures that applying the substitution will not permit any type
--   parameter to escape from its scope.
data Subst
emptySubst :: Subst
singleSubst :: TVar -> Type -> Subst
(@@) :: Subst -> Subst -> Subst

-- | A defaulting substitution maps all otherwise-unmapped free variables
--   to a kind-appropriate default type (Bit for value types and
--   0 for numeric types).
defaultingSubst :: Subst -> Subst

-- | 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

-- | Makes a substitution out of a list. WARNING: We do not validate the
--   list in any way, so the caller should ensure that we end up with a
--   valid (e.g., idempotent) substitution.
listParamSubst :: [(TParam, Type)] -> Subst
isEmptySubst :: Subst -> Bool
class FVS t
fvs :: FVS t => t -> Set TVar

-- | Apply a substitution. Returns Nothing if nothing changed.
apSubstMaybe :: Subst -> Type -> Maybe Type
class TVars t
apSubst :: TVars t => Subst -> t -> t

-- | Apply the substitution to the keys of a type map.
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
substBinds :: Subst -> Set TVar
applySubstToVar :: Subst -> TVar -> Maybe Type
substToList :: Subst -> [(TVar, Type)]
instance GHC.Show.Show Cryptol.TypeCheck.Subst.Subst
instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars (GHC.Maybe.Maybe t)
instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars [t]
instance (Cryptol.TypeCheck.Subst.TVars s, Cryptol.TypeCheck.Subst.TVars t) => Cryptol.TypeCheck.Subst.TVars (s, t)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Type.Type
instance (GHC.Base.Functor m, Cryptol.TypeCheck.Subst.TVars a) => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.List m a)
instance Cryptol.TypeCheck.Subst.TVars a => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.TypeMap a)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Type.Schema
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Expr
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Match
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Decl
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Subst.Subst)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Subst.Subst

module Cryptol.TypeCheck.Unify

-- | The most general unifier is a substitution and a set of constraints on
--   bound variables.
type MGU = (Subst, [Prop])
type Result a = Writer [UnificationError] a
runResult :: Result a -> (a, [UnificationError])
data UnificationError
UniTypeMismatch :: Type -> Type -> UnificationError
UniKindMismatch :: Kind -> Kind -> UnificationError
UniTypeLenMismatch :: Int -> Int -> UnificationError
UniRecursive :: TVar -> Type -> UnificationError
UniNonPolyDepends :: TVar -> [TParam] -> UnificationError
UniNonPoly :: TVar -> Type -> UnificationError
uniError :: UnificationError -> Result MGU
emptyMGU :: MGU
mgu :: Type -> Type -> Result MGU
mguMany :: [Type] -> [Type] -> Result MGU
bindVar :: TVar -> Type -> Result MGU
freeParams :: FVS t => t -> Set TParam

module Cryptol.TypeCheck.TypeOf

-- | Given a typing environment and an expression, compute the type of the
--   expression as quickly as possible, assuming that the expression is
--   well formed with correct type annotations.
fastTypeOf :: Map Name Schema -> Expr -> Type
fastSchemaOf :: Map Name Schema -> Expr -> Schema

-- | Assumes that local names do not shadow top level names.
module Cryptol.ModuleSystem.InstantiateModule

-- | Convert a module instantiation into a partial module. The resulting
--   module is incomplete because it is missing the definitions from the
--   instantiation.
instantiateModule :: FreshM m => Module -> ModName -> Map TParam Type -> Map Name Expr -> m ([Located Prop], Module)
instance GHC.Show.Show Cryptol.ModuleSystem.InstantiateModule.Env
instance Cryptol.ModuleSystem.InstantiateModule.Inst a => Cryptol.ModuleSystem.InstantiateModule.Inst [a]
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Expr
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Decl
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.AST.Match
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Schema
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Type
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.TCon.TCon
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.TCon.TC
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.TCon.UserTC
instance Cryptol.ModuleSystem.InstantiateModule.Inst (Cryptol.ModuleSystem.Exports.ExportSpec Cryptol.ModuleSystem.Name.Name)
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.TySyn
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.Newtype
instance Cryptol.ModuleSystem.InstantiateModule.Inst Cryptol.TypeCheck.Type.AbstractType
instance Cryptol.ModuleSystem.InstantiateModule.Defines t => Cryptol.ModuleSystem.InstantiateModule.Defines [t]
instance Cryptol.ModuleSystem.InstantiateModule.Defines Cryptol.TypeCheck.AST.Decl
instance Cryptol.ModuleSystem.InstantiateModule.Defines Cryptol.TypeCheck.AST.DeclGroup

-- | Look for opportunity to solve goals by instantiating variables.
module Cryptol.TypeCheck.Solver.Improve

-- | Improvements from a bunch of propositions. Invariant: the substitions
--   should be already applied to the new sub-goals, if any.
improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst, [Prop])

-- | Improvements from a proposition. Invariant: the substitions should be
--   already applied to the new sub-goals, if any.
improveProp :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
improveLit :: Bool -> Prop -> Match (Subst, [Prop])

-- | Improvements from equality constraints. Invariant: the substitions
--   should be already applied to the new sub-goals, if any.
improveEq :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])

-- | This module contains types used during type inference.
module Cryptol.TypeCheck.InferTypes
data SolverConfig
SolverConfig :: FilePath -> [String] -> Int -> [FilePath] -> SolverConfig

-- | The SMT solver to invoke
[solverPath] :: SolverConfig -> FilePath

-- | Additional arguments to pass to the solver
[solverArgs] :: SolverConfig -> [String]

-- | How verbose to be when type-checking
[solverVerbose] :: SolverConfig -> Int

-- | Look for the solver prelude in these locations.
[solverPreludePath] :: SolverConfig -> [FilePath]

-- | The types of variables in the environment.
data VarType

-- | Known type
ExtVar :: Schema -> VarType

-- | Part of current SCC. The expression will replace the variable, after
--   we are done with the SCC. In this way a variable that gets generalized
--   is replaced with an appropriate instantiation of itself.
CurSCC :: Expr -> Type -> VarType
data Goals
Goals :: Set Goal -> Map TVar LitGoal -> Goals

-- | A bunch of goals, not including the ones in literalGoals.
[goalSet] :: Goals -> Set Goal

-- | An entry (a,t) corresponds to Literal t a.
[literalGoals] :: Goals -> Map TVar LitGoal

-- | This abuses the type Goal a bit. The goal field contains
--   only the numeric part of the Literal constraint. For example, (a,
--   Goal { goal = t }) representats the goal for Literal t a
type LitGoal = Goal
litGoalToGoal :: (TVar, LitGoal) -> Goal
goalToLitGoal :: Goal -> Maybe (TVar, LitGoal)
emptyGoals :: Goals
nullGoals :: Goals -> Bool
fromGoals :: Goals -> [Goal]
goalsFromList :: [Goal] -> Goals
insertGoal :: Goal -> Goals -> Goals

-- | Something that we need to find evidence for.
data Goal
Goal :: ConstraintSource -> Range -> Prop -> Goal

-- | What it is about
[goalSource] :: Goal -> ConstraintSource

-- | Part of source code that caused goal
[goalRange] :: Goal -> Range

-- | What needs to be proved
[goal] :: Goal -> Prop
data HasGoal
HasGoal :: !Int -> Goal -> HasGoal
[hasName] :: HasGoal -> !Int
[hasGoal] :: HasGoal -> Goal

-- | A solution for a HasGoal
data HasGoalSln
HasGoalSln :: (Expr -> Expr) -> (Expr -> Expr -> Expr) -> HasGoalSln

-- | Select a specific field from the input expsression.
[hasDoSelect] :: HasGoalSln -> Expr -> Expr

-- | Set a field of the first expression to the second expression
[hasDoSet] :: HasGoalSln -> Expr -> Expr -> Expr

-- | Delayed implication constraints, arising from user-specified type
--   sigs.
data DelayedCt
DelayedCt :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt

-- | Signature that gave rise to this constraint Nothing means module
--   top-level
[dctSource] :: DelayedCt -> Maybe Name
[dctForall] :: DelayedCt -> [TParam]
[dctAsmps] :: DelayedCt -> [Prop]
[dctGoals] :: DelayedCt -> [Goal]

-- | Information about how a constraint came to be, used in error
--   reporting.
data ConstraintSource

-- | Computing shape of list comprehension
CtComprehension :: ConstraintSource

-- | Use of a split pattern
CtSplitPat :: ConstraintSource

-- | A type signature in a pattern or expression
CtTypeSig :: ConstraintSource

-- | Instantiation of this expression
CtInst :: Expr -> ConstraintSource
CtSelector :: ConstraintSource
CtExactType :: ConstraintSource
CtEnumeration :: ConstraintSource

-- | Just defaulting on the command line
CtDefaulting :: ConstraintSource

-- | Use of a partial type function.
CtPartialTypeFun :: Name -> ConstraintSource
CtImprovement :: ConstraintSource

-- | Constraints arising from type-checking patterns
CtPattern :: Doc -> ConstraintSource

-- | Instantiating a parametrized module
CtModuleInstance :: ModName -> ConstraintSource

-- | For use in error messages
cppKind :: Kind -> Doc
addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
ppUse :: Expr -> Doc
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goals
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.HasGoal
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.DelayedCt
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goal
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.ConstraintSource
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.ConstraintSource
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.ConstraintSource
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.SolverConfig
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.SolverConfig
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.SolverConfig
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goals
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.HasGoal
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.DelayedCt
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.DelayedCt
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.DelayedCt)
instance GHC.Classes.Eq Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Classes.Ord Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Goal)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.ConstraintSource
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.ConstraintSource

module Cryptol.TypeCheck.Solver.SMT

-- | An SMT solver packed with a logger for debugging.
data Solver

-- | Execute a computation with a fresh solver instance.
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a

-- | Assumes no And
isNumeric :: Prop -> Bool
debugBlock :: Solver -> String -> IO a -> IO a
debugLog :: DebugLog t => Solver -> t -> IO ()

-- | Returns goals that were not proved
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]

-- | Check if the given goals are known to be unsolvable.
checkUnsolvable :: Solver -> [Goal] -> IO Bool
tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])
shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
instance Cryptol.TypeCheck.Solver.SMT.Mk ()
instance Cryptol.TypeCheck.Solver.SMT.Mk GHC.Integer.Type.Integer
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.TVar
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.TCon.TCErrorMessage
instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type)
instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type)
instance Cryptol.TypeCheck.Solver.SMT.DebugLog GHC.Types.Char
instance Cryptol.TypeCheck.Solver.SMT.DebugLog a => Cryptol.TypeCheck.Solver.SMT.DebugLog [a]
instance Cryptol.TypeCheck.Solver.SMT.DebugLog a => Cryptol.TypeCheck.Solver.SMT.DebugLog (GHC.Maybe.Maybe a)
instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.Utils.PP.Doc
instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Solver.SMT.DebugLog Cryptol.TypeCheck.Subst.Subst

module Cryptol.TypeCheck.Error
cleanupErrors :: [(Range, Error)] -> [(Range, Error)]

-- | Should the first error suppress the next one.
subsumes :: Error -> Error -> Bool
data Warning
DefaultingKind :: TParam Name -> Kind -> Warning
DefaultingWildType :: Kind -> Warning
DefaultingTo :: TVarInfo -> Type -> Warning

-- | Various errors that might happen during type checking/inference
data Error

-- | Just say this
ErrorMsg :: Doc -> Error

-- | Expected kind, inferred kind
KindMismatch :: Kind -> Kind -> Error

-- | Number of extra parameters, kind of result (which should not be of the
--   form _ -> _)
TooManyTypeParams :: Int -> Kind -> Error

-- | A type variable was applied to some arguments.
TyVarWithParams :: Error

-- | Type-synonym, number of extra params
TooManyTySynParams :: Name -> Int -> Error

-- | Who is missing params, number of missing params
TooFewTyParams :: Name -> Int -> Error

-- | The type synonym declarations are recursive
RecursiveTypeDecls :: [Name] -> Error

-- | Expected type, inferred type
TypeMismatch :: Type -> Type -> Error

-- | Unification results in a recursive type
RecursiveType :: Type -> Type -> Error

-- | A constraint that we could not solve The boolean indicates if we know
--   that this constraint is impossible.
UnsolvedGoals :: Bool -> [Goal] -> Error

-- | A constraint (with context) that we could not solve
UnsolvedDelayedCt :: DelayedCt -> Error

-- | Type wild cards are not allowed in this context (e.g., definitions of
--   type synonyms).
UnexpectedTypeWildCard :: Error

-- | Unification variable depends on quantified variables that are not in
--   scope.
TypeVariableEscaped :: Type -> [TParam] -> Error

-- | Quantified type variables (of kind *) need to match the given type, so
--   it does not work for all types.
NotForAll :: TVar -> Type -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
UndefinedTypeParameter :: Located Ident -> Error
RepeatedTypeParameter :: Ident -> [Range] -> Error
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Error.Error
instance GHC.Generics.Generic Cryptol.TypeCheck.Error.Error
instance GHC.Show.Show Cryptol.TypeCheck.Error.Error
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Error.Warning
instance GHC.Generics.Generic Cryptol.TypeCheck.Error.Warning
instance GHC.Show.Show Cryptol.TypeCheck.Error.Warning
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Error.Error
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Error.Error
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Error.Error
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Error.Error)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Error.Warning
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Error.Warning
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Error.Warning
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Error.Warning)

module Cryptol.TypeCheck.Monad

-- | This is what's returned when we lookup variables during kind checking.
data LkpTyVar

-- | Locally bound variable.
TLocalVar :: TParam -> Maybe Kind -> LkpTyVar

-- | An outer binding.
TOuterVar :: TParam -> LkpTyVar
data KRW
KRW :: Map Name Kind -> [(ConstraintSource, [Prop])] -> KRW

-- | kinds of (known) vars.
[typeParams] :: KRW -> Map Name Kind
[kCtrs] :: KRW -> [(ConstraintSource, [Prop])]

-- | Do we allow wild cards in the given context.
data AllowWildCards
AllowWildCards :: AllowWildCards
NoWildCards :: AllowWildCards
data KRO
KRO :: Map Name TParam -> AllowWildCards -> KRO

-- | lazy map, with tparams.
[lazyTParams] :: KRO -> Map Name TParam

-- | are type-wild cards allowed?
[allowWild] :: KRO -> AllowWildCards
newtype KindM a
KM :: ReaderT KRO (StateT KRW InferM) a -> KindM a
[unKM] :: KindM a -> ReaderT KRO (StateT KRW InferM) a

-- | Read-write component of the monad.
data RW
RW :: ![(Range, Error)] -> ![(Range, Warning)] -> !Subst -> [Map Name Type] -> Map Int HasGoalSln -> !NameSeeds -> !Goals -> ![HasGoal] -> !Supply -> RW

-- | Collected errors
[iErrors] :: RW -> ![(Range, Error)]

-- | Collected warnings
[iWarnings] :: RW -> ![(Range, Warning)]

-- | Accumulated substitution
[iSubst] :: RW -> !Subst

-- | These keeps track of what existential type variables are available.
--   When we start checking a function, we push a new scope for its
--   arguments, and we pop it when we are done checking the function body.
--   The front element of the list is the current scope, which is the only
--   thing that will be modified, as follows. When we encounter a
--   existential type variable: 1. we look in all scopes to see if it is
--   already defined. 2. if it was not defined, we create a fresh type
--   variable, and we add it to the current scope. 3. it is an error if we
--   encounter an existential variable but we have no current scope.
[iExistTVars] :: RW -> [Map Name Type]

-- | Selector constraints that have been solved (ref. iSolvedSelectorsLazy)
[iSolvedHas] :: RW -> Map Int HasGoalSln
[iNameSeeds] :: RW -> !NameSeeds

-- | Ordinary constraints
[iCts] :: RW -> !Goals

-- | Tuple/record projection constraints. The Int is the "name" of
--   the constraint, used so that we can name it solution properly.
[iHasCts] :: RW -> ![HasGoal]
[iSupply] :: RW -> !Supply

-- | Read-only component of the monad.
data RO
RO :: Range -> Map Name VarType -> [TParam] -> Map Name (DefLoc, TySyn) -> Map Name (DefLoc, Newtype) -> Map Name (DefLoc, AbstractType) -> Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> Map Int HasGoalSln -> Bool -> Solver -> !PrimMap -> !IORef Int -> RO

-- | Source code being analysed
[iRange] :: RO -> Range

-- | Type of variable that are in scope
[iVars] :: RO -> Map Name VarType

-- | Type variable that are in scope
[iTVars] :: RO -> [TParam]

-- | Type synonyms that are in scope
[iTSyns] :: RO -> Map Name (DefLoc, TySyn)

-- | Newtype declarations in scope
--   
--   NOTE: type synonyms take precedence over newtype. The reason is that
--   we can define local type synonyms, but not local newtypes. So, either
--   a type-synonym shadows a newtype, or it was declared at the top-level,
--   but then there can't be a newtype with the same name (this should be
--   caught by the renamer).
[iNewtypes] :: RO -> Map Name (DefLoc, Newtype)
[iAbstractTypes] :: RO -> Map Name (DefLoc, AbstractType)

-- | Parameter types
[iParamTypes] :: RO -> Map Name ModTParam

-- | Constraints on the type parameters
[iParamConstraints] :: RO -> [Located Prop]

-- | Parameter functions
[iParamFuns] :: RO -> Map Name ModVParam

-- | NOTE: This field is lazy in an important way! It is the final version
--   of iSolvedHas in RW, and the two are tied together
--   through recursion. The field is here so that we can look thing up
--   before they are defined, which is OK because we don't need to know the
--   results until everything is done.
[iSolvedHasLazy] :: RO -> Map Int HasGoalSln

-- | When this flag is set to true, bindings that lack signatures in
--   where-blocks will never be generalized. Bindings with type signatures,
--   and all bindings at top level are unaffected.
[iMonoBinds] :: RO -> Bool
[iSolver] :: RO -> Solver
[iPrimNames] :: RO -> !PrimMap
[iSolveCounter] :: RO -> !IORef Int
data DefLoc
IsLocal :: DefLoc
IsExternal :: DefLoc
newtype InferM a
IM :: ReaderT RO (StateT RW IO) a -> InferM a
[unIM] :: InferM a -> ReaderT RO (StateT RW IO) a

-- | The results of type inference.
data InferOutput a

-- | We found some errors
InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a

-- | Type inference was successful.
InferOK :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a

-- | This is used for generating various names.
data NameSeeds
NameSeeds :: !Int -> !Int -> NameSeeds
[seedTVar] :: NameSeeds -> !Int
[seedGoal] :: NameSeeds -> !Int

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> Map Name AbstractType -> !Map Name ModTParam -> ![Located Prop] -> !Map Name ModVParam -> NameSeeds -> Bool -> SolverConfig -> [FilePath] -> !PrimMap -> !Supply -> InferInput

-- | Location of program source
[inpRange] :: InferInput -> Range

-- | Variables that are in scope
[inpVars] :: InferInput -> Map Name Schema

-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map Name TySyn

-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map Name Newtype

-- | Abstract types in scope
[inpAbstractTypes] :: InferInput -> Map Name AbstractType

-- | Type parameters
[inpParamTypes] :: InferInput -> !Map Name ModTParam

-- | Constraints on parameters
[inpParamConstraints] :: InferInput -> ![Located Prop]

-- | Value parameters
[inpParamFuns] :: InferInput -> !Map Name ModVParam

-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds

-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool

-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig

-- | Where to look for Cryptol theory file.
[inpSearchPath] :: InferInput -> [FilePath]

-- | This is used when the type-checker needs to refer to a predefined
--   identifier (e.g., number).
[inpPrimNames] :: InferInput -> !PrimMap

-- | The supply for fresh name generation
[inpSupply] :: InferInput -> !Supply

-- | The initial seeds, used when checking a fresh program. XXX: why does
--   this start at 10?
nameSeeds :: NameSeeds
bumpCounter :: InferM ()
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
io :: IO a -> InferM a

-- | The monadic computation is about the given range of source code. This
--   is useful for error reporting.
inRange :: Range -> InferM a -> InferM a
inRangeMb :: Maybe Range -> InferM a -> InferM a

-- | This is the current range that we are working on.
curRange :: InferM Range

-- | Report an error.
recordError :: Error -> InferM ()
recordWarning :: Warning -> InferM ()
getSolver :: InferM Solver

-- | Retrieve the mapping between identifiers and declarations in the
--   prelude.
getPrimMap :: InferM PrimMap
newGoal :: ConstraintSource -> Prop -> InferM Goal

-- | Record some constraints that need to be solved. The string explains
--   where the constraints came from.
newGoals :: ConstraintSource -> [Prop] -> InferM ()

-- | The constraints are removed, and returned to the caller. The
--   substitution IS applied to them.
getGoals :: InferM [Goal]

-- | Add a bunch of goals that need solving.
addGoals :: [Goal] -> InferM ()

-- | Collect the goals emitted by the given sub-computation. Does not emit
--   any new goals.
collectGoals :: InferM a -> InferM (a, [Goal])
simpGoal :: Goal -> InferM [Goal]
simpGoals :: [Goal] -> InferM [Goal]

-- | Record a constraint that when we select from the first type, we should
--   get a value of the second type. The returned function should be used
--   to wrap the expression from which we are selecting (i.e., the record
--   or tuple). Plese note that the resulting expression should not be
--   forced before the constraint is solved.
newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln

-- | 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 -&gt; Expr`) for the given constraint
--   (Int).
solveHasGoal :: Int -> HasGoalSln -> InferM ()

-- | Generate a fresh variable name to be used in a local binding.
newParamName :: Ident -> InferM Name
newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a

-- | Generate a new name for a goal.
newGoalName :: InferM Int

-- | Generate a new free type variable.
newTVar :: TVarSource -> Kind -> InferM TVar

-- | Generate a new free type variable that depends on these additional
--   type parameters.
newTVar' :: TVarSource -> Set TParam -> Kind -> InferM TVar

-- | Generate a new free type variable.
newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam

-- | Generate an unknown type. The doc is a note about what is this type
--   about.
newType :: TVarSource -> Kind -> InferM Type

-- | Record that the two types should be syntactically equal.
unify :: Type -> Type -> InferM [Prop]

-- | Apply the accumulated substitution to something with free type
--   variables.
applySubst :: TVars t => t -> InferM t
applySubstPreds :: [Prop] -> InferM [Prop]
applySubstGoals :: [Goal] -> InferM [Goal]

-- | Get the substitution that we have accumulated so far.
getSubst :: InferM Subst

-- | Add to the accumulated substitution, checking that the datatype
--   invariant for Subst is maintained.
extendSubst :: Subst -> InferM ()

-- | Variables that are either mentioned in the environment or in a
--   selector constraint.
varsWithAsmps :: InferM (Set TVar)

-- | Lookup the type of a variable.
lookupVar :: Name -> InferM VarType

-- | Lookup a type variable. Return Nothing if there is no such
--   variable in scope, in which case we must be dealing with a type
--   constant.
lookupTParam :: Name -> InferM (Maybe TParam)

-- | Lookup the definition of a type synonym.
lookupTSyn :: Name -> InferM (Maybe TySyn)

-- | Lookup the definition of a newtype
lookupNewtype :: Name -> InferM (Maybe Newtype)
lookupAbstractType :: Name -> InferM (Maybe AbstractType)

-- | Lookup the kind of a parameter type
lookupParamType :: Name -> InferM (Maybe ModTParam)

-- | Lookup the schema for a parameter function.
lookupParamFun :: Name -> InferM (Maybe ModVParam)

-- | Check if we already have a name for this existential type variable
--   and, if so, return the definition. If not, try to create a new
--   definition, if this is allowed. If not, returns nothing.
existVar :: Name -> Kind -> InferM Type

-- | Returns the type synonyms that are currently in scope.
getTSyns :: InferM (Map Name (DefLoc, TySyn))

-- | Returns the newtype declarations that are in scope.
getNewtypes :: InferM (Map Name (DefLoc, Newtype))

-- | Returns the abstract type declarations that are in scope.
getAbstractTypes :: InferM (Map Name (DefLoc, AbstractType))

-- | Returns the parameter functions declarations
getParamFuns :: InferM (Map Name ModVParam)

-- | Returns the abstract function declarations
getParamTypes :: InferM (Map Name ModTParam)

-- | Constraints on the module's parameters.
getParamConstraints :: InferM [Located Prop]

-- | Get the set of bound type variables that are in scope.
getTVars :: InferM (Set Name)

-- | Return the keys of the bound variables that are in scope.
getBoundInScope :: InferM (Set TParam)

-- | Retrieve the value of the `mono-binds` option.
getMonoBinds :: InferM Bool

-- | We disallow shadowing between type synonyms and type variables because
--   it is confusing. As a bonus, in the implementation we don't need to
--   worry about where we lookup things (i.e., in the variable or type
--   synonym environment.
checkTShadowing :: String -> Name -> InferM ()

-- | The sub-computation is performed with the given type parameter in
--   scope.
withTParam :: TParam -> InferM a -> InferM a
withTParams :: [TParam] -> InferM a -> InferM a

-- | The sub-computation is performed with the given type-synonym in scope.
withTySyn :: TySyn -> InferM a -> InferM a
withNewtype :: Newtype -> InferM a -> InferM a
withPrimType :: AbstractType -> InferM a -> InferM a
withParamType :: ModTParam -> InferM a -> InferM a

-- | The sub-computation is performed with the given variable in scope.
withVarType :: Name -> VarType -> InferM a -> InferM a
withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a
withVar :: Name -> Schema -> InferM a -> InferM a

-- | The sub-computation is performed with the given abstract function in
--   scope.
withParamFuns :: [ModVParam] -> InferM a -> InferM a

-- | Add some assumptions for an entire module
withParameterConstraints :: [Located Prop] -> InferM a -> InferM a

-- | The sub-computation is performed with the given variables in scope.
withMonoType :: (Name, Located Type) -> InferM a -> InferM a

-- | The sub-computation is performed with the given variables in scope.
withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a

-- | The sub-computation is performed with the given type synonyms and
--   variables in scope.
withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a

-- | Perform the given computation in a new scope (i.e., the subcomputation
--   may use existential type variables).
inNewScope :: InferM a -> InferM a

-- | The arguments to this function are as follows:
--   
--   (type param. name, kind signature (opt.), type parameter)
--   
--   The type parameter is just a thunk that we should not force. The
--   reason is that the parameter depends on the kind that we are in the
--   process of computing.
--   
--   As a result we return the value of the sub-computation and the
--   computed kinds of the type parameters.
runKindM :: AllowWildCards -> [(Name, Maybe Kind, TParam)] -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])

-- | Check if a name refers to a type variable.
kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)

-- | Are type wild-cards OK in this context?
kWildOK :: KindM AllowWildCards

-- | Reports an error.
kRecordError :: Error -> KindM ()
kRecordWarning :: Warning -> KindM ()
kIO :: IO a -> KindM a

-- | Generate a fresh unification variable of the given kind. NOTE: We do
--   not simplify these, because we end up with bottom. See hs XXX:
--   Perhaps we can avoid the recursion?
kNewType :: TVarSource -> Kind -> KindM Type

-- | Lookup the definition of a type synonym.
kLookupTSyn :: Name -> KindM (Maybe TySyn)

-- | Lookup the definition of a newtype.
kLookupNewtype :: Name -> KindM (Maybe Newtype)
kLookupParamType :: Name -> KindM (Maybe ModTParam)
kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
kExistTVar :: Name -> Kind -> KindM Type

-- | Replace the given bound variables with concrete types.
kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type

-- | Record the kind for a local type variable. This assumes that we
--   already checked that there was no other valid kind for the variable
--   (if there was one, it gets over-written).
kSetKind :: Name -> Kind -> KindM ()

-- | The sub-computation is about the given range of the source code.
kInRange :: Range -> KindM a -> KindM a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kInInferM :: InferM a -> KindM a
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.Monad.InferOutput a)
instance GHC.Show.Show Cryptol.TypeCheck.Monad.InferInput
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Generics.Generic Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Show.Show Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Base.Functor Cryptol.TypeCheck.Monad.KindM
instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.KindM
instance GHC.Base.Monad Cryptol.TypeCheck.Monad.KindM
instance Control.Monad.Fail.MonadFail Cryptol.TypeCheck.Monad.KindM
instance GHC.Base.Functor Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Monad Cryptol.TypeCheck.Monad.InferM
instance Control.Monad.Fail.MonadFail Cryptol.TypeCheck.Monad.InferM
instance Control.Monad.Fix.MonadFix Cryptol.TypeCheck.Monad.InferM
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.TypeCheck.Monad.InferM

module Cryptol.TypeCheck.Solver.Selector

-- | Solve has-constraints.
tryHasGoal :: HasGoal -> InferM (Bool, Bool)

module Cryptol.TypeCheck.Sanity
tcExpr :: InferInput -> Expr -> Either Error (Schema, [ProofObligation])
tcDecls :: InferInput -> [DeclGroup] -> Either Error [ProofObligation]
tcModule :: InferInput -> Module -> Either Error [ProofObligation]
type ProofObligation = Schema
data Error

-- | expected, actual
TypeMismatch :: String -> Schema -> Schema -> Error

-- | expected a mono type, got this
ExpectedMono :: Schema -> Error
TupleSelectorOutOfRange :: Int -> Int -> Error
MissingField :: Ident -> [Ident] -> Error
UnexpectedTupleShape :: Int -> Int -> Error
UnexpectedRecordShape :: [Ident] -> [Ident] -> Error
UnexpectedSequenceShape :: Int -> Type -> Error
BadSelector :: Selector -> Type -> Error
BadInstantiation :: Error
Captured :: TVar -> Error
BadProofNoAbs :: Error
BadProofTyVars :: [TParam] -> Error
KindMismatch :: Kind -> Kind -> Error
NotEnoughArgumentsInKind :: Kind -> Error
BadApplication :: Type -> Type -> Error
FreeTypeVariable :: TVar -> Error
BadTypeApplication :: Kind -> [Kind] -> Error
RepeatedVariableInForall :: TParam -> Error
BadMatch :: Type -> Error
EmptyArm :: Error
UndefinedTypeVaraible :: TVar -> Error
UndefinedVariable :: Name -> Error
same :: Same a => a -> a -> Bool
instance GHC.Show.Show Cryptol.TypeCheck.Sanity.Error
instance GHC.Base.Functor Cryptol.TypeCheck.Sanity.TcM
instance GHC.Base.Applicative Cryptol.TypeCheck.Sanity.TcM
instance GHC.Base.Monad Cryptol.TypeCheck.Sanity.TcM
instance Cryptol.TypeCheck.Sanity.Same a => Cryptol.TypeCheck.Sanity.Same [a]
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.Schema
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.TParam

module Cryptol.TypeCheck.Depends
data TyDecl

-- | Type synonym
TS :: TySyn Name -> Maybe String -> TyDecl

-- | Newtype
NT :: Newtype Name -> Maybe String -> TyDecl

-- | Parameter type
AT :: ParameterType Name -> Maybe String -> TyDecl

-- | Property synonym
PS :: PropSyn Name -> Maybe String -> TyDecl

-- | A primitive/abstract typee
PT :: PrimType Name -> Maybe String -> TyDecl
setDocString :: Maybe String -> TyDecl -> TyDecl

-- | Check for duplicate and recursive type synonyms. Returns the
--   type-synonyms in dependency order.
orderTyDecls :: [TyDecl] -> InferM [TyDecl]

-- | Associate type signatures with bindings and order bindings by
--   dependency.
orderBinds :: [Bind Name] -> [SCC (Bind Name)]
class FromDecl d
toBind :: FromDecl d => d -> Maybe (Bind Name)
toParamFun :: FromDecl d => d -> Maybe (ParameterFun Name)
toParamConstraints :: FromDecl d => d -> [Located (Prop Name)]
toTyDecl :: FromDecl d => d -> Maybe TyDecl
isTopDecl :: FromDecl d => d -> Bool

-- | Given a list of declarations, annoted with (i) the names that they
--   define, and (ii) the names that they use, we compute a list of
--   strongly connected components of the declarations. The SCCs are in
--   dependency order.
mkScc :: [(a, [Name], [Name])] -> [SCC a]

-- | Combine a bunch of definitions into a single map. Here we check that
--   each name is defined only onces.
combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a))

-- | Combine a bunch of definitions into a single map. Here we check that
--   each name is defined only onces.
combine :: [(Name, Located a)] -> InferM (Map Name (Located a))

-- | Identify multiple occurances of something.
duplicates :: Ord a => [Located a] -> [(a, [Range])]
instance GHC.Show.Show Cryptol.TypeCheck.Depends.TyDecl
instance Cryptol.TypeCheck.Depends.FromDecl (Cryptol.Parser.AST.TopDecl Cryptol.ModuleSystem.Name.Name)
instance Cryptol.TypeCheck.Depends.FromDecl (Cryptol.Parser.AST.Decl Cryptol.ModuleSystem.Name.Name)

module Cryptol.TypeCheck.Default

-- | We default constraints of the form Literal t a to a :=
--   [width t]
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])

-- | Try to pick a reasonable instantiation for an expression with the
--   given type. This is useful when we do evaluation at the REPL. The
--   resulting types should satisfy the constraints of the schema. The
--   parameters should be all of numeric kind, and the props should als be
--   numeric
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)])

module Cryptol.TypeCheck.Solve
simplifyAllConstraints :: InferM ()

-- | Prove an implication, and return any improvements that we computed.
--   Records errors, if any of the goals couldn't be solved.
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst

-- | Try to clean-up any left-over constraints after we've checked
--   everything in a module. Typically these are either trivial things, or
--   constraints on the module's type parameters.
proveModuleTopLevel :: InferM ()
defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))

module Cryptol.TypeCheck.Kind
checkType :: Type Name -> Maybe Kind -> InferM Type

-- | Check a type signature. Returns validated schema, and any implicit
--   constraints that we inferred.
checkSchema :: AllowWildCards -> Schema Name -> InferM (Schema, [Goal])

-- | Check a newtype declaration. XXX: Do something with constraints.
checkNewtype :: Newtype Name -> Maybe String -> InferM Newtype
checkPrimType :: PrimType Name -> Maybe String -> InferM AbstractType

-- | Check a type-synonym declaration.
checkTySyn :: TySyn Name -> Maybe String -> InferM TySyn

-- | Check a constraint-synonym declaration.
checkPropSyn :: PropSyn Name -> Maybe String -> InferM TySyn

-- | Check a module parameter declarations. Nothing much to check, we just
--   translate from one syntax to another.
checkParameterType :: ParameterType Name -> Maybe String -> InferM ModTParam
checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop]

module Cryptol.TypeCheck.Instantiate
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)
data TypeArg
TypeArg :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
[tyArgName] :: TypeArg -> Maybe (Located Ident)
[tyArgType] :: TypeArg -> MaybeCheckedType
uncheckedTypeArg :: TypeInst Name -> TypeArg
data MaybeCheckedType
Checked :: Type -> MaybeCheckedType
Unchecked :: Type Name -> MaybeCheckedType

-- | Assumes that the NoPat pass has been run.
module Cryptol.TypeCheck.Infer

-- | Infer the type of an expression, and translate it to a fully
--   elaborated core term.
checkE :: Expr Name -> Type -> InferM Expr
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
inferModule :: Module Name -> InferM Module

-- | inferBinds isTopLevel isRec binds performs inference for a
--   strongly-connected component of Binds. If any of the members of
--   the recursive group are already marked as monomorphic, then we don't
--   do generalzation. If isTopLevel is true, any bindings without
--   type signatures will be generalized. If it is false, and the
--   mono-binds flag is enabled, no bindings without type signatures will
--   be generalized, but bindings with signatures will be unaffected.
inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a

module Cryptol.TypeCheck.CheckModuleInstance

-- | Check that the instance provides what the functor needs.
checkModuleInstance :: Module -> Module -> InferM Module

module Cryptol.TypeCheck
tcModule :: Module Name -> InferInput -> IO (InferOutput Module)

-- | Check a module instantiation, assuming that the functor has already
--   been checked.
tcModuleInst :: Module -> Module Name -> InferInput -> IO (InferOutput Module)
tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> Map Name AbstractType -> !Map Name ModTParam -> ![Located Prop] -> !Map Name ModVParam -> NameSeeds -> Bool -> SolverConfig -> [FilePath] -> !PrimMap -> !Supply -> InferInput

-- | Location of program source
[inpRange] :: InferInput -> Range

-- | Variables that are in scope
[inpVars] :: InferInput -> Map Name Schema

-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map Name TySyn

-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map Name Newtype

-- | Abstract types in scope
[inpAbstractTypes] :: InferInput -> Map Name AbstractType

-- | Type parameters
[inpParamTypes] :: InferInput -> !Map Name ModTParam

-- | Constraints on parameters
[inpParamConstraints] :: InferInput -> ![Located Prop]

-- | Value parameters
[inpParamFuns] :: InferInput -> !Map Name ModVParam

-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds

-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool

-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig

-- | Where to look for Cryptol theory file.
[inpSearchPath] :: InferInput -> [FilePath]

-- | This is used when the type-checker needs to refer to a predefined
--   identifier (e.g., number).
[inpPrimNames] :: InferInput -> !PrimMap

-- | The supply for fresh name generation
[inpSupply] :: InferInput -> !Supply

-- | The results of type inference.
data InferOutput a

-- | We found some errors
InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a

-- | Type inference was successful.
InferOK :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
data SolverConfig
SolverConfig :: FilePath -> [String] -> Int -> [FilePath] -> SolverConfig

-- | The SMT solver to invoke
[solverPath] :: SolverConfig -> FilePath

-- | Additional arguments to pass to the solver
[solverArgs] :: SolverConfig -> [String]

-- | How verbose to be when type-checking
[solverVerbose] :: SolverConfig -> Int

-- | Look for the solver prelude in these locations.
[solverPreludePath] :: SolverConfig -> [FilePath]

-- | This is used for generating various names.
data NameSeeds

-- | The initial seeds, used when checking a fresh program. XXX: why does
--   this start at 10?
nameSeeds :: NameSeeds

-- | Various errors that might happen during type checking/inference
data Error

-- | Just say this
ErrorMsg :: Doc -> Error

-- | Expected kind, inferred kind
KindMismatch :: Kind -> Kind -> Error

-- | Number of extra parameters, kind of result (which should not be of the
--   form _ -> _)
TooManyTypeParams :: Int -> Kind -> Error

-- | A type variable was applied to some arguments.
TyVarWithParams :: Error

-- | Type-synonym, number of extra params
TooManyTySynParams :: Name -> Int -> Error

-- | Who is missing params, number of missing params
TooFewTyParams :: Name -> Int -> Error

-- | The type synonym declarations are recursive
RecursiveTypeDecls :: [Name] -> Error

-- | Expected type, inferred type
TypeMismatch :: Type -> Type -> Error

-- | Unification results in a recursive type
RecursiveType :: Type -> Type -> Error

-- | A constraint that we could not solve The boolean indicates if we know
--   that this constraint is impossible.
UnsolvedGoals :: Bool -> [Goal] -> Error

-- | A constraint (with context) that we could not solve
UnsolvedDelayedCt :: DelayedCt -> Error

-- | Type wild cards are not allowed in this context (e.g., definitions of
--   type synonyms).
UnexpectedTypeWildCard :: Error

-- | Unification variable depends on quantified variables that are not in
--   scope.
TypeVariableEscaped :: Type -> [TParam] -> Error

-- | Quantified type variables (of kind *) need to match the given type, so
--   it does not work for all types.
NotForAll :: TVar -> Type -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
UndefinedTypeParameter :: Located Ident -> Error
RepeatedTypeParameter :: Ident -> [Range] -> Error
data Warning
DefaultingKind :: TParam Name -> Kind -> Warning
DefaultingWildType :: Kind -> Warning
DefaultingTo :: TVarInfo -> Type -> Warning
ppWarning :: (Range, Warning) -> Doc
ppError :: (Range, Error) -> Doc

module Cryptol.ModuleSystem.Env

-- | This is the current state of the interpreter.
data ModuleEnv
ModuleEnv :: LoadedModules -> NameSeeds -> SolverConfig -> EvalEnv -> CoreLint -> !Bool -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Supply -> ModuleEnv

-- | Information about all loaded modules. See LoadedModule.
--   Contains information such as the file where the module was loaded
--   from, as well as the module's interface, used for type checking.
[meLoadedModules] :: ModuleEnv -> LoadedModules

-- | A source of new names for the type checker.
[meNameSeeds] :: ModuleEnv -> NameSeeds

-- | Configuration settings for the SMT solver used for type-checking.
[meSolverConfig] :: ModuleEnv -> SolverConfig

-- | The evaluation environment. Contains the values for all loaded
--   modules, both public and private.
[meEvalEnv] :: ModuleEnv -> EvalEnv

-- | Should we run the linter to ensure sanity.
[meCoreLint] :: ModuleEnv -> CoreLint

-- | Are we assuming that local bindings are monomorphic. XXX: We should
--   probably remove this flag, and set it to True.
[meMonoBinds] :: ModuleEnv -> !Bool

-- | The "current" module. Used to decide how to print names, for example.
[meFocusedModule] :: ModuleEnv -> Maybe ModName

-- | Where we look for things.
[meSearchPath] :: ModuleEnv -> [FilePath]

-- | This contains additional definitions that were made at the command
--   line, and so they don't reside in any module.
[meDynEnv] :: ModuleEnv -> DynamicEnv

-- | Name source for the renamer
[meSupply] :: ModuleEnv -> !Supply

-- | Should we run the linter?
data CoreLint

-- | Don't run core lint
NoCoreLint :: CoreLint

-- | Run core lint
CoreLint :: CoreLint
resetModuleEnv :: ModuleEnv -> ModuleEnv
initialModuleEnv :: IO ModuleEnv

-- | Try to focus a loaded module in the module environment.
focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv

-- | Get a list of all the loaded modules. Each module in the resulting
--   list depends only on other modules that precede it. Note that this
--   includes parameterized modules.
loadedModules :: ModuleEnv -> [Module]

-- | Get a list of all the loaded non-parameterized modules. These are the
--   modules that can be used for evaluation, proving etc.
loadedNonParamModules :: ModuleEnv -> [Module]

-- | Are any parameterized modules loaded?
hasParamModules :: ModuleEnv -> Bool

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system, as well as a NameDisp for pretty-printing names
--   according to the imports.
--   
--   XXX This could really do with some better error handling, just
--   returning mempty when one of the imports fails isn't really desirable.
--   
--   XXX: This is not quite right. For example, it does not take into
--   account *how* things were imported in a module (e.g., qualified). It
--   would be simpler to simply store the naming environment that was
--   actually used when we renamed the module.
focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)

-- | The unqualified declarations and name environment for the dynamic
--   environment.
dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)

-- | The location of a module
data ModulePath
InFile :: FilePath -> ModulePath

-- | Label, content
InMem :: String -> ByteString -> ModulePath

-- | The name of the content---either the file path, or the provided label.
modulePathLabel :: ModulePath -> String
data LoadedModules
LoadedModules :: [LoadedModule] -> [LoadedModule] -> LoadedModules

-- | Invariants: 1) All the dependencies of any module m must
--   precede m in the list. 2) Does not contain any parameterized
--   modules.
[lmLoadedModules] :: LoadedModules -> [LoadedModule]

-- | Loaded parameterized modules.
[lmLoadedParamModules] :: LoadedModules -> [LoadedModule]
getLoadedModules :: LoadedModules -> [LoadedModule]
data LoadedModule
LoadedModule :: ModName -> ModulePath -> String -> Iface -> Module -> Fingerprint -> LoadedModule
[lmName] :: LoadedModule -> ModName

-- | The file path used to load this module (may not be canonical)
[lmFilePath] :: LoadedModule -> ModulePath

-- | An identifier used to identify the source of the bytes for the module.
--   For files we just use the cononical path, for in memory things we use
--   their label.
[lmModuleId] :: LoadedModule -> String
[lmInterface] :: LoadedModule -> Iface
[lmModule] :: LoadedModule -> Module
[lmFingerprint] :: LoadedModule -> Fingerprint

-- | Has this module been loaded already.
isLoaded :: ModName -> LoadedModules -> Bool

-- | Is this a loaded parameterized module.
isLoadedParamMod :: ModName -> LoadedModules -> Bool

-- | Try to find a previously loaded module
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule

-- | Add a freshly loaded module. If it was previously loaded, then the new
--   version is ignored.
addLoadedModule :: ModulePath -> String -> Fingerprint -> Module -> LoadedModules -> LoadedModules

-- | Remove a previously loaded module.
removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules

-- | Extra information we need to carry around to dynamically extend an
--   environment outside the context of a single module. Particularly
--   useful when dealing with interactive declarations as in :let
--   or it.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv

-- | Build IfaceDecls that correspond to all of the bindings in the
--   dynamic environment.
--   
--   XXX: if we ever add type synonyms or newtypes at the REPL, revisit
--   this.
deIfaceDecls :: DynamicEnv -> IfaceDecls
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.ModuleEnv
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.DynamicEnv
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.DynamicEnv
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModules
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModule
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModule
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModule
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.ModulePath
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.ModulePath
instance GHC.Show.Show Cryptol.ModuleSystem.Env.ModulePath
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.CoreLint
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.CoreLint
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.ModuleEnv
instance GHC.Base.Semigroup Cryptol.ModuleSystem.Env.DynamicEnv
instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.DynamicEnv
instance GHC.Base.Semigroup Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Classes.Eq Cryptol.ModuleSystem.Env.ModulePath
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Env.ModulePath

module Cryptol.Version
commitHash :: String
commitShortHash :: String
commitBranch :: String
commitDirty :: Bool
version :: Version

module Cryptol.Parser
parseModule :: Config -> Text -> Either ParseError (Module PName)
parseProgram :: Layout -> Text -> Either ParseError (Program PName)
parseProgramWith :: Config -> Text -> Either ParseError (Program PName)
parseExpr :: Text -> Either ParseError (Expr PName)
parseExprWith :: Config -> Text -> Either ParseError (Expr PName)
parseDecl :: Text -> Either ParseError (Decl PName)
parseDeclWith :: Config -> Text -> Either ParseError (Decl PName)
parseDecls :: Text -> Either ParseError [Decl PName]
parseDeclsWith :: Config -> Text -> Either ParseError [Decl PName]
parseLetDecl :: Text -> Either ParseError (Decl PName)
parseLetDeclWith :: Config -> Text -> Either ParseError (Decl PName)
parseRepl :: Text -> Either ParseError (ReplInput PName)
parseReplWith :: Config -> Text -> Either ParseError (ReplInput PName)
parseSchema :: Text -> Either ParseError (Schema PName)
parseSchemaWith :: Config -> Text -> Either ParseError (Schema PName)
parseModName :: String -> Maybe ModName
parseHelpName :: String -> Maybe PName
data ParseError
HappyError :: FilePath -> Located Token -> ParseError
HappyErrorMsg :: Range -> String -> ParseError
HappyUnexpected :: FilePath -> Maybe (Located Token) -> String -> ParseError
HappyOutOfTokens :: FilePath -> Position -> ParseError
ppError :: ParseError -> Doc
data Layout
Layout :: Layout
NoLayout :: Layout
data Config
Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config

-- | File that we are working on
[cfgSource] :: Config -> !FilePath

-- | Settings for layout processing
[cfgLayout] :: Config -> !Layout

-- | Preprocessor settings
[cfgPreProc] :: Config -> PreProc

-- | Implicit includes
[cfgAutoInclude] :: Config -> [FilePath]

-- | When we do layout processing should we add a vCurly (i.e., are we
--   parsing a list of things).
[cfgModuleScope] :: Config -> Bool
defaultConfig :: Config
guessPreProc :: FilePath -> PreProc
data PreProc
None :: PreProc
Markdown :: PreProc
LaTeX :: PreProc

module Cryptol.Parser.NoInclude
removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
data IncludeError
IncludeFailed :: Located FilePath -> IncludeError
IncludeParseError :: ParseError -> IncludeError
IncludeCycle :: [Located FilePath] -> IncludeError
ppIncludeError :: IncludeError -> Doc
instance Control.DeepSeq.NFData Cryptol.Parser.NoInclude.IncludeError
instance GHC.Generics.Generic Cryptol.Parser.NoInclude.IncludeError
instance GHC.Show.Show Cryptol.Parser.NoInclude.IncludeError
instance GHC.Base.Functor Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Applicative Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Monad Cryptol.Parser.NoInclude.NoIncM
instance Control.Monad.Fail.MonadFail Cryptol.Parser.NoInclude.NoIncM

module Cryptol.ModuleSystem.Monad
data ImportSource
FromModule :: ModName -> ImportSource
FromImport :: Located Import -> ImportSource
FromModuleInstance :: Located ModName -> ImportSource
importedModule :: ImportSource -> ModName
data ModuleError

-- | Unable to find the module given, tried looking in these paths
ModuleNotFound :: ModName -> [FilePath] -> ModuleError

-- | Unable to open a file
CantFindFile :: FilePath -> ModuleError

-- | Bad UTF-8 encoding in while decoding this file
BadUtf8 :: ModulePath -> UnicodeException -> 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 :: ModulePath -> ParseError -> ModuleError

-- | Recursive module group discovered
RecursiveModules :: [ImportSource] -> ModuleError

-- | Problems during the renaming phase
RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError

-- | Problems during the NoPat phase
NoPatErrors :: ImportSource -> [Error] -> ModuleError

-- | Problems during the NoInclude phase
NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError

-- | Problems during type checking
TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError

-- | Problems after type checking, eg. specialization
OtherFailure :: String -> ModuleError

-- | Module loaded by 'import' statement has the wrong module name
ModuleNameMismatch :: ModName -> Located ModName -> ModuleError

-- | Two modules loaded from different files have the same module name
DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError

-- | Attempt to import a parametrized module that was not instantiated.
ImportedParamModule :: ModName -> ModuleError

-- | Failed to add the module parameters to all definitions in a module.
FailedToParameterizeModDefs :: ModName -> [Name] -> ModuleError
NotAParameterizedModule :: ModName -> ModuleError

-- | This is just a tag on the error, indicating the file containing it. It
--   is convenient when we had to look for the module, and we'd like to
--   communicate the location of pthe problematic module to the handler.
ErrorInFile :: ModulePath -> ModuleError -> ModuleError
moduleNotFound :: ModName -> [FilePath] -> ModuleM a
cantFindFile :: FilePath -> ModuleM a
badUtf8 :: ModulePath -> UnicodeException -> ModuleM a
otherIOError :: FilePath -> IOException -> ModuleM a
moduleParseError :: ModulePath -> ParseError -> ModuleM a
recursiveModules :: [ImportSource] -> ModuleM a
renamerErrors :: [RenamerError] -> ModuleM a
noPatErrors :: [Error] -> ModuleM a
noIncludeErrors :: [IncludeError] -> ModuleM a
typeCheckingFailed :: [(Range, Error)] -> ModuleM a
moduleNameMismatch :: ModName -> Located ModName -> ModuleM a
duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a
importParamModule :: ModName -> ModuleM a
failedToParameterizeModDefs :: ModName -> [Name] -> ModuleM a
notAParameterizedModule :: ModName -> ModuleM a

-- | Run the computation, and if it caused and error, tag the error with
--   the given file.
errorInFile :: ModulePath -> ModuleM a -> ModuleM a
data ModuleWarning
TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning
RenamerWarnings :: [RenamerWarning] -> ModuleWarning
warn :: [ModuleWarning] -> ModuleM ()
typeCheckWarnings :: [(Range, Warning)] -> ModuleM ()
renamerWarnings :: [RenamerWarning] -> ModuleM ()
data RO
RO :: [ImportSource] -> EvalOpts -> RO
[roLoading] :: RO -> [ImportSource]
[roEvalOpts] :: RO -> EvalOpts
emptyRO :: EvalOpts -> RO
newtype ModuleT m a
ModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a -> ModuleT m a
[unModuleT] :: ModuleT m a -> ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
runModuleT :: Monad m => (EvalOpts, ModuleEnv) -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
type ModuleM = ModuleT IO
runModuleM :: (EvalOpts, ModuleEnv) -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
io :: BaseM m IO => IO a -> ModuleT m a
getModuleEnv :: Monad m => ModuleT m ModuleEnv
setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m ()
getLoadedMaybe :: ModName -> ModuleM (Maybe LoadedModule)
isLoaded :: ModName -> ModuleM Bool
loadingImport :: Located Import -> ModuleM a -> ModuleM a
loadingModule :: ModName -> ModuleM a -> ModuleM a
loadingModInstance :: Located ModName -> ModuleM a -> ModuleM a

-- | Push an "interactive" context onto the loading stack. A bit of a hack,
--   as it uses a faked module name
interactive :: ModuleM a -> ModuleM a
loading :: ImportSource -> ModuleM a -> ModuleM a

-- | Get the currently focused import source.
getImportSource :: ModuleM ImportSource
getIface :: ModName -> ModuleM Iface
getLoaded :: ModName -> ModuleM Module
getNameSeeds :: ModuleM NameSeeds
getSupply :: ModuleM Supply
getMonoBinds :: ModuleM Bool
setMonoBinds :: Bool -> ModuleM ()
setNameSeeds :: NameSeeds -> ModuleM ()
setSupply :: Supply -> ModuleM ()
unloadModule :: (LoadedModule -> Bool) -> ModuleM ()
loadedModule :: ModulePath -> Fingerprint -> Module -> ModuleM ()
modifyEvalEnv :: (EvalEnv -> Eval EvalEnv) -> ModuleM ()
getEvalEnv :: ModuleM EvalEnv
getEvalOpts :: ModuleM EvalOpts
getFocusedModule :: ModuleM (Maybe ModName)
setFocusedModule :: ModName -> ModuleM ()
getSearchPath :: ModuleM [FilePath]

-- | Run a ModuleM action in a context with a prepended search path.
--   Useful for temporarily looking in other places while resolving
--   imports, for example.
withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
getFocusedEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getDynEnv :: ModuleM DynamicEnv
setDynEnv :: DynamicEnv -> ModuleM ()
setSolver :: SolverConfig -> ModuleM ()
getSolverConfig :: ModuleM SolverConfig

-- | Usefule for logging. For example: withLogger logPutStrLn
--   Hello
withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleError
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Monad.ModuleT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Monad.ModuleT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Monad.ModuleT m)
instance Control.Monad.Fail.MonadFail m => Control.Monad.Fail.MonadFail (Cryptol.ModuleSystem.Monad.ModuleT m)
instance MonadLib.MonadT Cryptol.ModuleSystem.Monad.ModuleT
instance GHC.Base.Monad m => Cryptol.ModuleSystem.Name.FreshM (Cryptol.ModuleSystem.Monad.ModuleT m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Cryptol.ModuleSystem.Monad.ModuleT m)
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleWarning
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleError
instance GHC.Classes.Eq Cryptol.ModuleSystem.Monad.ImportSource
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ImportSource

-- | This is the main driver---it provides entry points for the various
--   passes.
module Cryptol.ModuleSystem.Base
rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a

-- | Rename a module in the context of its imported modules.
renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
parseModule :: ModulePath -> ModuleM (Fingerprint, Module PName)

-- | Load a module by its path.
loadModuleByPath :: FilePath -> ModuleM Module

-- | Load a module, unless it was previously loaded.
loadModuleFrom :: ImportSource -> ModuleM (ModulePath, Module)

-- | Load dependencies, typecheck, and add to the eval environment.
doLoadModule :: ImportSource -> ModulePath -> Fingerprint -> Module PName -> ModuleM Module

-- | Rewrite an import declaration to be of the form:
--   
--   
--   import foo as foo [ [hiding] (a,b,c) ]
--   
fullyQualified :: Import -> Import

-- | Find the interface referenced by an import, and generate the naming
--   environment that it describes.
importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)

-- | Load a series of interfaces, merging their public interfaces.
importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)
moduleFile :: ModName -> String -> FilePath

-- | Discover a module.
findModule :: ModName -> ModuleM ModulePath

-- | Discover a file. This is distinct from findModule in that we
--   assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath

-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: Module PName -> Module PName

-- | Load the dependencies of a module into the environment.
loadDeps :: Module name -> ModuleM ()

-- | Load the local environment, which consists of the environment for the
--   currently opened module, shadowed by the dynamic environment.
getLocalEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv)

-- | Typecheck a single expression, yielding a renamed parsed expression,
--   typechecked core expression, and a type schema.
checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema)

-- | Typecheck a group of declarations.
--   
--   INVARIANT: This assumes that NoPat has already been run on the
--   declarations.
checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])

-- | Generate the primitive map. If the prelude is currently being loaded,
--   this should be generated directly from the naming environment given to
--   the renamer instead.
getPrimMap :: ModuleM PrimMap

-- | Load a module, be it a normal module or a functor instantiation.
checkModule :: ImportSource -> ModulePath -> Module PName -> ModuleM Module

-- | Typecheck a single module. If the module is an instantiation of a
--   functor, then this just type-checks the instantiating parameters. See
--   checkModule
checkSingleModule :: Act (Module Name) Module -> ImportSource -> ModulePath -> Module PName -> ModuleM Module
data TCLinter o
TCLinter :: (o -> InferInput -> Either Error [ProofObligation]) -> Maybe ModName -> TCLinter o
[lintCheck] :: TCLinter o -> o -> InferInput -> Either Error [ProofObligation]
[lintModule] :: TCLinter o -> Maybe ModName
exprLinter :: TCLinter (Expr, Schema)
declsLinter :: TCLinter [DeclGroup]
moduleLinter :: ModName -> TCLinter Module
type Act i o = i -> InferInput -> IO (InferOutput o)
data TCAction i o
TCAction :: Act i o -> TCLinter o -> PrimMap -> TCAction i o
[tcAction] :: TCAction i o -> Act i o
[tcLinter] :: TCAction i o -> TCLinter o
[tcPrims] :: TCAction i o -> PrimMap
typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o

-- | Generate input for the typechecker.
genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput
evalExpr :: Expr -> ModuleM Value
evalDecls :: [DeclGroup] -> ModuleM ()

module Cryptol.ModuleSystem

-- | This is the current state of the interpreter.
data ModuleEnv
ModuleEnv :: LoadedModules -> NameSeeds -> SolverConfig -> EvalEnv -> CoreLint -> !Bool -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Supply -> ModuleEnv

-- | Information about all loaded modules. See LoadedModule.
--   Contains information such as the file where the module was loaded
--   from, as well as the module's interface, used for type checking.
[meLoadedModules] :: ModuleEnv -> LoadedModules

-- | A source of new names for the type checker.
[meNameSeeds] :: ModuleEnv -> NameSeeds

-- | Configuration settings for the SMT solver used for type-checking.
[meSolverConfig] :: ModuleEnv -> SolverConfig

-- | The evaluation environment. Contains the values for all loaded
--   modules, both public and private.
[meEvalEnv] :: ModuleEnv -> EvalEnv

-- | Should we run the linter to ensure sanity.
[meCoreLint] :: ModuleEnv -> CoreLint

-- | Are we assuming that local bindings are monomorphic. XXX: We should
--   probably remove this flag, and set it to True.
[meMonoBinds] :: ModuleEnv -> !Bool

-- | The "current" module. Used to decide how to print names, for example.
[meFocusedModule] :: ModuleEnv -> Maybe ModName

-- | Where we look for things.
[meSearchPath] :: ModuleEnv -> [FilePath]

-- | This contains additional definitions that were made at the command
--   line, and so they don't reside in any module.
[meDynEnv] :: ModuleEnv -> DynamicEnv

-- | Name source for the renamer
[meSupply] :: ModuleEnv -> !Supply
initialModuleEnv :: IO ModuleEnv

-- | Extra information we need to carry around to dynamically extend an
--   environment outside the context of a single module. Particularly
--   useful when dealing with interactive declarations as in :let
--   or it.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv
data ModuleError

-- | Unable to find the module given, tried looking in these paths
ModuleNotFound :: ModName -> [FilePath] -> ModuleError

-- | Unable to open a file
CantFindFile :: FilePath -> ModuleError

-- | Bad UTF-8 encoding in while decoding this file
BadUtf8 :: ModulePath -> UnicodeException -> 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 :: ModulePath -> ParseError -> ModuleError

-- | Recursive module group discovered
RecursiveModules :: [ImportSource] -> ModuleError

-- | Problems during the renaming phase
RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError

-- | Problems during the NoPat phase
NoPatErrors :: ImportSource -> [Error] -> ModuleError

-- | Problems during the NoInclude phase
NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError

-- | Problems during type checking
TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError

-- | Problems after type checking, eg. specialization
OtherFailure :: String -> ModuleError

-- | Module loaded by 'import' statement has the wrong module name
ModuleNameMismatch :: ModName -> Located ModName -> ModuleError

-- | Two modules loaded from different files have the same module name
DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError

-- | Attempt to import a parametrized module that was not instantiated.
ImportedParamModule :: ModName -> ModuleError

-- | Failed to add the module parameters to all definitions in a module.
FailedToParameterizeModDefs :: ModName -> [Name] -> ModuleError
NotAParameterizedModule :: ModName -> ModuleError

-- | This is just a tag on the error, indicating the file containing it. It
--   is convenient when we had to look for the module, and we'd like to
--   communicate the location of pthe problematic module to the handler.
ErrorInFile :: ModulePath -> ModuleError -> ModuleError
data ModuleWarning
TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning
RenamerWarnings :: [RenamerWarning] -> ModuleWarning
type ModuleCmd a = (EvalOpts, ModuleEnv) -> IO (ModuleRes a)
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])

-- | Find the file associated with a module name in the module search path.
findModule :: ModName -> ModuleCmd ModulePath

-- | Load the module contained in the given file.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module)

-- | Load the given parsed module.
loadModuleByName :: ModName -> ModuleCmd (ModulePath, Module)

-- | Check the type of an expression. Give back the renamed expression, the
--   core expression, and its type schema.
checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)

-- | Evaluate an expression.
evalExpr :: Expr -> ModuleCmd Value

-- | Typecheck top-level declarations.
checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])

-- | Evaluate declarations and add them to the extended environment.
evalDecls :: [DeclGroup] -> ModuleCmd ()
noPat :: RemovePatterns a => a -> ModuleCmd a

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system, as well as a NameDisp for pretty-printing names
--   according to the imports.
--   
--   XXX This could really do with some better error handling, just
--   returning mempty when one of the imports fails isn't really desirable.
--   
--   XXX: This is not quite right. For example, it does not take into
--   account *how* things were imported in a module (e.g., qualified). It
--   would be simpler to simply store the naming environment that was
--   actually used when we renamed the module.
focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getPrimMap :: ModuleCmd PrimMap
renameVar :: NamingEnv -> PName -> ModuleCmd Name
renameType :: NamingEnv -> PName -> ModuleCmd Name

-- | The resulting interface generated by a module that has been
--   typechecked.
data Iface
Iface :: !ModName -> IfaceDecls -> IfaceDecls -> IfaceParams -> Iface

-- | Module name
[ifModName] :: Iface -> !ModName

-- | Exported definitions
[ifPublic] :: Iface -> IfaceDecls

-- | Private defintiions
[ifPrivate] :: Iface -> IfaceDecls

-- | Uninterpreted constants (aka module params)
[ifParams] :: Iface -> IfaceParams
data IfaceParams
IfaceParams :: Map Name ModTParam -> [Located Prop] -> Map Name ModVParam -> IfaceParams
[ifParamTypes] :: IfaceParams -> Map Name ModTParam

-- | Constraints on param. types
[ifParamConstraints] :: IfaceParams -> [Located Prop]
[ifParamFuns] :: IfaceParams -> Map Name ModVParam
data IfaceDecls
IfaceDecls :: Map Name IfaceTySyn -> Map Name IfaceNewtype -> Map Name IfaceAbstractType -> Map Name IfaceDecl -> IfaceDecls
[ifTySyns] :: IfaceDecls -> Map Name IfaceTySyn
[ifNewtypes] :: IfaceDecls -> Map Name IfaceNewtype
[ifAbstractTypes] :: IfaceDecls -> Map Name IfaceAbstractType
[ifDecls] :: IfaceDecls -> Map Name IfaceDecl

-- | Generate an Iface from a typechecked module.
genIface :: Module -> Iface
type IfaceTySyn = TySyn
data IfaceDecl
IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl

-- | Name of thing
[ifDeclName] :: IfaceDecl -> !Name

-- | Type
[ifDeclSig] :: IfaceDecl -> Schema

-- | Pragmas
[ifDeclPragmas] :: IfaceDecl -> [Pragma]

-- | Is this an infix thing
[ifDeclInfix] :: IfaceDecl -> Bool

-- | Fixity information
[ifDeclFixity] :: IfaceDecl -> Maybe Fixity

-- | Documentation
[ifDeclDoc] :: IfaceDecl -> Maybe String

module Cryptol.Transform.Specialize

-- | A Name should have an entry in the SpecCache iff it is specializable.
--   Each Name starts out with an empty TypesMap.
type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl))

-- | The specializer monad.
type SpecT m a = StateT SpecCache (ModuleT m) a
type SpecM a = SpecT IO a
runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
liftSpecT :: Monad m => ModuleT m a -> SpecT m a
getSpecCache :: Monad m => SpecT m SpecCache
setSpecCache :: Monad m => SpecCache -> SpecT m ()
modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m ()
modify :: StateM m s => (s -> s) -> m ()

-- | Add a `where` clause to the given expression containing
--   type-specialized versions of all functions called (transitively) by
--   the body of the expression.
specialize :: Expr -> ModuleCmd Expr
specializeExpr :: Expr -> SpecM Expr
specializeMatch :: Match -> SpecM Match

-- | Add the declarations to the SpecCache, run the given monadic action,
--   and then pull the specialized declarations back out of the SpecCache
--   state. Return the result along with the declarations and a table of
--   names of specialized bindings.
withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))

-- | Compute the specialization of `EWhere e dgs`. A decl within
--   dgs is replicated once for each monomorphic type instance at
--   which it is used; decls not mentioned in e (even monomorphic
--   ones) are simply dropped.
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr

-- | Transform the given declaration groups into a set of monomorphic
--   declarations. All of the original declarations with monomorphic types
--   are kept; additionally the result set includes instantiated versions
--   of polymorphic decls that are referenced by the monomorphic bindings.
--   We also return a map relating generated names to the names from the
--   original declarations.
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name))
specializeConst :: Expr -> SpecM Expr
destEProofApps :: Expr -> (Expr, Int)
destETApps :: Expr -> (Expr, [Type])
destEProofAbs :: Expr -> ([Prop], Expr)
destETAbs :: Expr -> ([TParam], Expr)

-- | Freshen a name by giving it a new unique.
freshName :: Name -> [Type] -> SpecM Name
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema

-- | Reduce `length ts` outermost type abstractions and n proof
--   abstractions.
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
allDeclGroups :: ModuleEnv -> [DeclGroup]
traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)

module Cryptol.Symbolic
type EvalEnv = GenEvalEnv SBool SWord
proverConfigs :: [(String, SMTConfig)]
proverNames :: [String]
lookupProver :: String -> SMTConfig
type SatResult = [(Type, Expr, Value)]
data SatNum
AllSat :: SatNum
SomeSat :: Int -> SatNum
data QueryType
SatQuery :: SatNum -> QueryType
ProveQuery :: QueryType
data ProverCommand
ProverCommand :: QueryType -> String -> Bool -> Bool -> !IORef ProverStats -> [DeclGroup] -> Maybe FilePath -> Expr -> Schema -> ProverCommand

-- | The type of query to run
[pcQueryType] :: ProverCommand -> QueryType

-- | Which prover to use (one of the strings in proverConfigs)
[pcProverName] :: ProverCommand -> String

-- | Verbosity flag passed to SBV
[pcVerbose] :: ProverCommand -> Bool

-- | Model validation flag passed to SBV
[pcValidate] :: ProverCommand -> Bool

-- | Record timing information here
[pcProverStats] :: ProverCommand -> !IORef ProverStats

-- | Extra declarations to bring into scope for symbolic simulation
[pcExtraDecls] :: ProverCommand -> [DeclGroup]

-- | Optionally output the SMTLIB query to a file
[pcSmtFile] :: ProverCommand -> Maybe FilePath

-- | The typechecked expression to evaluate
[pcExpr] :: ProverCommand -> Expr

-- | The Schema of pcExpr
[pcSchema] :: ProverCommand -> Schema
type ProverStats = NominalDiffTime

-- | A prover result is either an error message, an empty result (eg for
--   the offline prover), a counterexample or a lazy list of satisfying
--   assignments.
data ProverResult
AllSatResult :: [SatResult] -> ProverResult
ThmResult :: [Type] -> ProverResult
EmptyResult :: ProverResult
ProverError :: String -> ProverResult
satSMTResults :: SatResult -> [SMTResult]
allSatSMTResults :: AllSatResult -> [SMTResult]
thmSMTResults :: ThmResult -> [SMTResult]
proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)
satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
parseValues :: [FinType] -> [CV] -> ([Value], [CV])
parseValue :: FinType -> [CV] -> (Value, [CV])
allDeclGroups :: ModuleEnv -> [DeclGroup]
data FinType
FTBit :: FinType
FTInteger :: FinType
FTIntMod :: Integer -> FinType
FTSeq :: Int -> FinType -> FinType
FTTuple :: [FinType] -> FinType
FTRecord :: [(Ident, FinType)] -> FinType
numType :: Integer -> Maybe Int
finType :: TValue -> Maybe FinType
unFinType :: FinType -> Type
predArgTypes :: Schema -> Either String [FinType]
inBoundsIntMod :: Integer -> SInteger -> SBool
forallFinType :: FinType -> WriterT [SBool] Symbolic Value
existsFinType :: FinType -> WriterT [SBool] Symbolic Value
instance GHC.Show.Show Cryptol.Symbolic.QueryType
instance GHC.Show.Show Cryptol.Symbolic.SatNum

module Cryptol.REPL.Monad

-- | REPL_ context with InputT handling.
newtype REPL a
REPL :: (IORef RW -> IO a) -> REPL a
[unREPL] :: REPL a -> IORef RW -> IO a

-- | Run a REPL action with a fresh environment.
runREPL :: Bool -> Logger -> REPL a -> IO a
io :: IO a -> REPL a

-- | Raise an exception.
raise :: REPLException -> REPL a
stop :: REPL ()
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
finally :: REPL a -> REPL b -> REPL a

-- | Use the configured output action to print a string with a trailing
--   newline
rPutStrLn :: String -> REPL ()

-- | Use the configured output action to print a string
rPutStr :: String -> REPL ()

-- | Use the configured output action to print something using its Show
--   instance
rPrint :: Show a => a -> REPL ()

-- | REPL exceptions.
data REPLException
ParseError :: ParseError -> REPLException
FileNotFound :: FilePath -> REPLException
DirectoryNotFound :: FilePath -> REPLException
NoPatError :: [Error] -> REPLException
NoIncludeError :: [IncludeError] -> REPLException
EvalError :: EvalError -> REPLException
ModuleSystemError :: NameDisp -> ModuleError -> REPLException
EvalPolyError :: Schema -> REPLException
TypeNotTestable :: Type -> REPLException
EvalInParamModule :: [Name] -> REPLException
SBVError :: String -> REPLException
rethrowEvalError :: IO a -> IO a
getFocusedEnv :: REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getModuleEnv :: REPL ModuleEnv
setModuleEnv :: ModuleEnv -> REPL ()
getDynEnv :: REPL DynamicEnv
setDynEnv :: DynamicEnv -> REPL ()

-- | Given an existing qualified name, prefix it with a relatively-unique
--   string. We make it unique by prefixing with a character #
--   that is not lexically valid in a module name.
uniqify :: Name -> REPL Name

-- | Generate a fresh name using the given index. The name will reside
--   within the "interactive" namespace.
freshName :: Ident -> NameSource -> REPL Name
getTSyns :: REPL (Map Name TySyn)
getNewtypes :: REPL (Map Name Newtype)
getVars :: REPL (Map Name IfaceDecl)
whenDebug :: REPL () -> REPL ()

-- | Get visible variable names.
getExprNames :: REPL [String]

-- | Get visible type signature names.
getTypeNames :: REPL [String]

-- | Return a list of property names, sorted by position in the file.
getPropertyNames :: REPL ([Name], NameDisp)
getModNames :: REPL [ModName]

-- | This indicates what the user would like to work on.
data LoadedModule
LoadedModule :: Maybe ModName -> ModulePath -> LoadedModule

-- | Working on this module.
[lName] :: LoadedModule -> Maybe ModName

-- | Working on this file.
[lPath] :: LoadedModule -> ModulePath
getLoadedMod :: REPL (Maybe LoadedModule)

-- | Set the name of the currently focused file, loaded via :r.
setLoadedMod :: LoadedModule -> REPL ()
clearLoadedMod :: REPL ()

-- | Set the path for the ':e' command. Note that this does not change the
--   focused module (i.e., what ":r" reloads)
setEditPath :: FilePath -> REPL ()
getEditPath :: REPL (Maybe FilePath)
clearEditPath :: REPL ()
setSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [FilePath] -> REPL ()

-- | Construct the prompt for the current environment.
getPrompt :: REPL String
shouldContinue :: REPL Bool
unlessBatch :: REPL () -> REPL ()

-- | Run a computation in batch mode, restoring the previous isBatch flag
--   afterwards
asBatch :: REPL a -> REPL a
disableLet :: REPL ()
enableLet :: REPL ()

-- | Are let-bindings enabled in this REPL?
getLetEnabled :: REPL Bool

-- | Is evaluation enabled. If the currently focused module is
--   parameterized, then we cannot evalute.
validEvalContext :: FreeVars a => a -> REPL ()

-- | Update the title
updateREPLTitle :: REPL ()

-- | Set the function that will be called when updating the title
setUpdateREPLTitle :: REPL () -> REPL ()
data EnvVal
EnvString :: String -> EnvVal
EnvProg :: String -> [String] -> EnvVal
EnvNum :: !Int -> EnvVal
EnvBool :: Bool -> EnvVal
data OptionDescr
OptionDescr :: String -> EnvVal -> Checker -> String -> (EnvVal -> REPL ()) -> OptionDescr
[optName] :: OptionDescr -> String
[optDefault] :: OptionDescr -> EnvVal
[optCheck] :: OptionDescr -> Checker
[optHelp] :: OptionDescr -> String
[optEff] :: OptionDescr -> EnvVal -> REPL ()

-- | Set a user option.
setUser :: String -> String -> REPL ()

-- | Get a user option, when it's known to exist. Fail with panic when it
--   doesn't.
getUser :: String -> REPL EnvVal
getKnownUser :: IsEnvVal a => String -> REPL a

-- | Get a user option, using Maybe for failure.
tryGetUser :: String -> REPL (Maybe EnvVal)
userOptions :: OptionMap
getUserSatNum :: REPL SatNum
getUserShowProverStats :: REPL Bool
getUserProverValidate :: REPL Bool

-- | Get the REPL's string-printer
getPutStr :: REPL (String -> IO ())
getLogger :: REPL Logger

-- | Set the REPL's string-printer
setPutStr :: (String -> IO ()) -> REPL ()
smokeTest :: REPL [Smoke]
data Smoke
Z3NotFound :: Smoke
instance GHC.Classes.Eq Cryptol.REPL.Monad.Smoke
instance GHC.Show.Show Cryptol.REPL.Monad.Smoke
instance GHC.Show.Show Cryptol.REPL.Monad.EnvVal
instance GHC.Show.Show Cryptol.REPL.Monad.REPLException
instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.Smoke
instance Cryptol.REPL.Monad.IsEnvVal GHC.Types.Bool
instance Cryptol.REPL.Monad.IsEnvVal GHC.Types.Int
instance Cryptol.REPL.Monad.IsEnvVal (GHC.Base.String, [GHC.Base.String])
instance Cryptol.REPL.Monad.IsEnvVal GHC.Base.String
instance GHC.Base.Functor Cryptol.REPL.Monad.REPL
instance GHC.Base.Applicative Cryptol.REPL.Monad.REPL
instance GHC.Base.Monad Cryptol.REPL.Monad.REPL
instance Control.Monad.IO.Class.MonadIO Cryptol.REPL.Monad.REPL
instance Control.Monad.Base.MonadBase GHC.Types.IO Cryptol.REPL.Monad.REPL
instance Control.Monad.Trans.Control.MonadBaseControl GHC.Types.IO Cryptol.REPL.Monad.REPL
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.REPL.Monad.REPL
instance GHC.Exception.Type.Exception Cryptol.REPL.Monad.REPLException
instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.REPLException

module Cryptol.Eval.Reference

-- | Value type for the reference evaluator.
data Value

-- |  Bit  booleans
VBit :: Either EvalError Bool -> Value

-- |  Integer  integers
VInteger :: Either EvalError Integer -> Value

-- |  [n]a  finite or infinite lists
VList :: Nat' -> [Value] -> Value

-- |  ( .. )  tuples
VTuple :: [Value] -> Value

-- |  { .. }  records
VRecord :: [(Ident, Value)] -> Value

-- | functions
VFun :: (Value -> Value) -> Value

-- | polymorphic values (kind *)
VPoly :: (TValue -> Value) -> Value

-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Value) -> Value
evaluate :: Expr -> ModuleCmd Value
ppValue :: PPOpts -> Value -> Doc
instance GHC.Base.Semigroup Cryptol.Eval.Reference.Env
instance GHC.Base.Monoid Cryptol.Eval.Reference.Env

module Cryptol.REPL.Command

-- | Commands.
data Command

-- | Successfully parsed command
Command :: REPL () -> Command

-- | Ambiguous command, list of conflicting commands
Ambiguous :: String -> [String] -> Command

-- | The unknown command
Unknown :: String -> Command

-- | Command builder.
data CommandDescr
CommandDescr :: [String] -> [String] -> CommandBody -> String -> CommandDescr
[cNames] :: CommandDescr -> [String]
[cArgs] :: CommandDescr -> [String]
[cBody] :: CommandDescr -> CommandBody
[cHelp] :: CommandDescr -> String
data CommandBody
ExprArg :: (String -> REPL ()) -> CommandBody
FileExprArg :: (FilePath -> String -> REPL ()) -> CommandBody
DeclsArg :: (String -> REPL ()) -> CommandBody
ExprTypeArg :: (String -> REPL ()) -> CommandBody
ModNameArg :: (String -> REPL ()) -> CommandBody
FilenameArg :: (FilePath -> REPL ()) -> CommandBody
OptionArg :: (String -> REPL ()) -> CommandBody
ShellArg :: (String -> REPL ()) -> CommandBody
HelpArg :: (String -> REPL ()) -> CommandBody
NoArg :: REPL () -> CommandBody
data CommandExitCode
CommandOk :: CommandExitCode
CommandError :: CommandExitCode

-- | Parse a line as a command.
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command

-- | Run a command.
runCommand :: Command -> REPL CommandExitCode

-- | Split at the first word boundary.
splitCommand :: String -> Maybe (String, String)

-- | Lookup a string in the command list.
findCommand :: String -> [CommandDescr]

-- | Lookup a string in the command list, returning an exact match even if
--   it's the prefix of another command.
findCommandExact :: String -> [CommandDescr]

-- | Lookup a string in the notebook-safe command list.
findNbCommand :: Bool -> String -> [CommandDescr]
commandList :: [CommandDescr]
moduleCmd :: String -> REPL ()
loadCmd :: FilePath -> REPL ()
loadPrelude :: REPL ()
setOptionCmd :: String -> REPL ()
interactiveConfig :: Config
replParseExpr :: String -> REPL (Expr PName)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)

-- | Randomly test a property, or exhaustively check it if the number of
--   values in the type under test is smaller than the tests
--   environment variable, or we specify exhaustive testing.
qcCmd :: QCMode -> String -> REPL [TestReport]
data QCMode
QCRandom :: QCMode
QCExhaust :: QCMode
satCmd :: String -> REPL ()
proveCmd :: String -> REPL ()
onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats)
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
handleCtrlC :: a -> REPL a

-- | Strip leading space.
sanitize :: String -> String

-- | Lift a parsing action into the REPL monad.
replParse :: (String -> Either ParseError a) -> String -> REPL a
liftModuleCmd :: ModuleCmd a -> REPL a
moduleCmdResult :: ModuleRes a -> REPL a
instance GHC.Show.Show Cryptol.REPL.Command.QCMode
instance GHC.Classes.Eq Cryptol.REPL.Command.QCMode
instance GHC.Show.Show Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Eq Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Ord Cryptol.REPL.Command.CommandDescr
