-- 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
--   <a>http://www.cryptol.net/</a>.
@package cryptol
@version 2.2.6


module Cryptol.Version
commitHash :: String
commitShortHash :: String
commitBranch :: String
commitDirty :: Bool


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

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


module Cryptol.Utils.Panic
panic :: String -> [String] -> a
instance GHC.Show.Show Cryptol.Utils.Panic.CryptolPanic
instance GHC.Exception.Exception Cryptol.Utils.Panic.CryptolPanic


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

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

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

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

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

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

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

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

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

-- | Compute the number of bits required to represent the given integer.
widthInteger :: Integer -> Integer
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Show.Show Cryptol.TypeCheck.Solver.InfNat.Nat'


-- | This module defines intervals and interval arithmetic.
module Cryptol.TypeCheck.Solver.Interval

-- | Representation of intervals. Intervals always include the lower bound.
--   Intervals include the upper bound if: * either the upper bound is
--   finite, or * the upper bound is <a>Inf</a> and <tt>isFinite ==
--   False</tt>.
--   
--   Invariant: if the upper bound is finite, then `isFinite == True`.
--   
--   <pre>
--   [x,y]     Interval (Nat x) (Nat y) True
--   [x,inf]   Interval (Nat x) Inf     False
--   [x,inf)   Interval (Nat x) Inf     True
--   </pre>
data Interval
Interval :: Nat' -> Nat' -> Bool -> Interval

-- | Lower bound
[lowerBound] :: Interval -> Nat'

-- | Upper bound
[upperBound] :: Interval -> Nat'

-- | Do we know this to be a finite value. Note that for <tt>[inf,inf]</tt>
--   this field is <a>False</a> (i.e., this field is not talking about the
--   size of the interval, but, rather, about if it contains infinity).
[isFinite] :: Interval -> Bool

-- | Any possible value.
anything :: Interval
iConst :: Nat' -> Interval
iAdd :: Interval -> Interval -> Interval
iMul :: Interval -> Interval -> Interval
iExp :: Interval -> Interval -> Interval
iMin :: Interval -> Interval -> Interval
iMax :: Interval -> Interval -> Interval
iLg2 :: Interval -> Interval
iWidth :: Interval -> Interval
iSub :: Interval -> Interval -> Interval
iDiv :: Interval -> Interval -> Interval
iMod :: Interval -> Interval -> Interval
iLenFromThen :: Interval -> Interval -> Interval -> Interval
iLenFromTo :: Interval -> Interval -> Interval
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval

-- | The first interval is definiately smaller
iLeq :: Interval -> Interval -> Bool

-- | The first interval is definiately smaller
iLt :: Interval -> Interval -> Bool

-- | The two intervals do not overlap.
iDisjoint :: Interval -> Interval -> Bool
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Interval.Interval


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


module Cryptol.TypeCheck.Solver.CrySAT
debug :: PropSet -> [S]
data Prop
Fin :: Expr -> Prop
(:==) :: Expr -> Expr -> Prop
(:/=) :: Expr -> Expr -> Prop
(:>=) :: Expr -> Expr -> Prop
(:>) :: Expr -> Expr -> Prop
(:&&) :: Prop -> Prop -> Prop
(:||) :: Prop -> Prop -> Prop
Not :: Prop -> Prop
data Expr
K :: InfNat -> Expr
Var :: Name -> Expr
(:+) :: Expr -> Expr -> Expr
(:-) :: Expr -> Expr -> Expr
(:*) :: Expr -> Expr -> Expr
Div :: Expr -> Expr -> Expr
Mod :: Expr -> Expr -> Expr
(:^^) :: Expr -> Expr -> Expr
Min :: Expr -> Expr -> Expr
Max :: Expr -> Expr -> Expr
Lg2 :: Expr -> Expr
Width :: Expr -> Expr
LenFromThen :: Expr -> Expr -> Expr -> Expr
LenFromThenTo :: Expr -> Expr -> Expr -> Expr
data PropSet
noProps :: PropSet
assert :: Prop -> PropSet -> PropSet
checkSat :: PropSet -> Result
data Result
Sat :: [(Int, InfNat)] -> Result
Unsat :: Result
Unknown :: Result
data InfNat
Nat :: Integer -> InfNat
Inf :: InfNat
data Name
toName :: Int -> Name
fromName :: Name -> Maybe Int
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.NonLin
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Result
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Prop
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Expr
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.InfNat
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.CrySAT.InfNat
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.CrySAT.InfNat
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.CrySAT.Name
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.CrySAT.Name
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Name
instance GHC.Base.Functor Cryptol.TypeCheck.Solver.CrySAT.FM
instance GHC.Base.Applicative Cryptol.TypeCheck.Solver.CrySAT.FM
instance GHC.Base.Alternative Cryptol.TypeCheck.Solver.CrySAT.FM
instance GHC.Base.Monad Cryptol.TypeCheck.Solver.CrySAT.FM
instance GHC.Base.MonadPlus Cryptol.TypeCheck.Solver.CrySAT.FM


module Cryptol.REPL.Trie

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

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

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

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

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


module Cryptol.Utils.PP
class PP a
ppPrec :: PP a => Int -> a -> Doc
pp :: PP a => a -> Doc
pretty :: PP a => a -> String
optParens :: Bool -> Doc -> Doc

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

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

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

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

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

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

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

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

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

-- | The suffix to use when displaying a number as an oridinal
ordSuffix :: (Integral a, Eq a) => a -> String
commaSep :: [Doc] -> Doc
instance GHC.Classes.Eq Cryptol.Utils.PP.Assoc
instance GHC.Show.Show Cryptol.Utils.PP.Assoc


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

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

module Cryptol.Parser.Lexer

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

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

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

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

-- | identifier
Ident :: String -> TokenT

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

-- | keyword
KW :: TokenKW -> TokenT

-- | operator
Op :: TokenOp -> TokenT

-- | symbol
Sym :: TokenSym -> TokenT

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

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

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

-- | Virtual tokens, inserted by layout processing.
data TokenV
VCurlyL :: TokenV
VCurlyR :: TokenV
VSemi :: TokenV
data TokenKW
KW_Arith :: TokenKW
KW_Bit :: TokenKW
KW_Cmp :: TokenKW
KW_False :: TokenKW
KW_True :: TokenKW
KW_else :: TokenKW
KW_Eq :: TokenKW
KW_error :: TokenKW
KW_extern :: TokenKW
KW_fin :: TokenKW
KW_if :: TokenKW
KW_private :: TokenKW
KW_include :: TokenKW
KW_inf :: TokenKW
KW_join :: TokenKW
KW_lg2 :: TokenKW
KW_lengthFromThen :: TokenKW
KW_lengthFromThenTo :: TokenKW
KW_max :: TokenKW
KW_min :: TokenKW
KW_module :: TokenKW
KW_newtype :: TokenKW
KW_pragma :: TokenKW
KW_pmult :: TokenKW
KW_pdiv :: TokenKW
KW_pmod :: TokenKW
KW_property :: TokenKW
KW_random :: TokenKW
KW_reverse :: TokenKW
KW_split :: TokenKW
KW_splitAt :: TokenKW
KW_then :: TokenKW
KW_transpose :: TokenKW
KW_type :: TokenKW
KW_where :: TokenKW
KW_let :: TokenKW
KW_x :: TokenKW
KW_zero :: TokenKW
KW_import :: TokenKW
KW_as :: TokenKW
KW_hiding :: TokenKW
data TokenErr
UnterminatedComment :: TokenErr
UnterminatedString :: TokenErr
UnterminatedChar :: TokenErr
InvalidString :: TokenErr
InvalidChar :: TokenErr
LexicalError :: TokenErr
data TokenOp
Plus :: TokenOp
Minus :: TokenOp
Mul :: TokenOp
Div :: TokenOp
Exp :: TokenOp
Mod :: TokenOp
NotEqual :: TokenOp
Equal :: TokenOp
LessThan :: TokenOp
GreaterThan :: TokenOp
LEQ :: TokenOp
GEQ :: TokenOp
EqualFun :: TokenOp
NotEqualFun :: TokenOp
ShiftL :: TokenOp
ShiftR :: TokenOp
RotL :: TokenOp
RotR :: TokenOp
Conj :: TokenOp
Disj :: TokenOp
Xor :: TokenOp
Complement :: TokenOp
Bang :: TokenOp
BangBang :: TokenOp
At :: TokenOp
AtAt :: TokenOp
Hash :: TokenOp
data TokenSym
Bar :: TokenSym
ArrL :: TokenSym
ArrR :: TokenSym
FatArrR :: TokenSym
Lambda :: TokenSym
EqDef :: TokenSym
Comma :: TokenSym
Semi :: TokenSym
Dot :: TokenSym
DotDot :: TokenSym
DotDotDot :: TokenSym
Colon :: TokenSym
ColonColon :: TokenSym
BackTick :: TokenSym
ParenL :: TokenSym
ParenR :: TokenSym
BracketL :: TokenSym
BracketR :: TokenSym
CurlyL :: TokenSym
CurlyR :: TokenSym
TriL :: TokenSym
TriR :: TokenSym
Underscore :: TokenSym
data TokenW
BlockComment :: TokenW
LineComment :: TokenW
Space :: TokenW
data Located a
Located :: !Range -> a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> a
data Config
Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config

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

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

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

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

-- | When we do layout processing should we add a vCurly (i.e., are we
--   parsing a list of things).
[cfgModuleScope] :: Config -> Bool
defaultConfig :: Config
instance GHC.Base.Functor Cryptol.Parser.Lexer.AlexLastAcc


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


module Cryptol.TypeCheck.PP
type NameMap = IntMap String

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

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


module Cryptol.Prims.Syntax

-- | Built-in types.
data TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCAdd :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCSub :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMul :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCDiv :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMod :: TFun

-- | <pre>
--   : Num -&gt; Num
--   </pre>
TCLg2 :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCExp :: TFun

-- | <pre>
--   : Num -&gt; Num
--   </pre>
TCWidth :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMin :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMax :: TFun

-- | <tt> : Num -&gt; Num -&gt; Num -&gt; Num</tt> Example: <tt>[ 1, 5 .. ]
--   :: [lengthFromThen 1 5 b][b]</tt>
TCLenFromThen :: TFun

-- | <tt> : Num -&gt; Num -&gt; Num -&gt; Num</tt> Example: <tt>[ 1, 5 .. 9
--   ] :: [lengthFromThenTo 1 5 9][b]</tt>
TCLenFromThenTo :: TFun

-- | Built-in constants.
data ECon
ECTrue :: ECon
ECFalse :: ECon

-- | Converts a numeric type into its corresponding value.
ECDemote :: ECon
ECPlus :: ECon
ECMinus :: ECon
ECMul :: ECon
ECDiv :: ECon
ECMod :: ECon
ECExp :: ECon
ECLg2 :: ECon
ECNeg :: ECon
ECLt :: ECon
ECGt :: ECon
ECLtEq :: ECon
ECGtEq :: ECon
ECEq :: ECon
ECNotEq :: ECon
ECFunEq :: ECon
ECFunNotEq :: ECon
ECMin :: ECon
ECMax :: ECon
ECAnd :: ECon
ECOr :: ECon
ECXor :: ECon
ECCompl :: ECon
ECZero :: ECon
ECShiftL :: ECon
ECShiftR :: ECon
ECRotL :: ECon
ECRotR :: ECon
ECCat :: ECon
ECSplitAt :: ECon
ECJoin :: ECon
ECSplit :: ECon
ECReverse :: ECon
ECTranspose :: ECon
ECAt :: ECon
ECAtRange :: ECon
ECAtBack :: ECon
ECAtRangeBack :: ECon
ECFromThen :: ECon
ECFromTo :: ECon
ECFromThenTo :: ECon
ECInfFrom :: ECon
ECInfFromThen :: ECon
ECError :: ECon
ECPMul :: ECon
ECPDiv :: ECon
ECPMod :: ECon
ECRandom :: ECon
eBinOpPrec :: Map ECon (Assoc, Int)
tBinOpPrec :: Map TFun (Assoc, Int)
ppPrefix :: ECon -> Doc
instance GHC.Enum.Enum Cryptol.Prims.Syntax.ECon
instance GHC.Enum.Bounded Cryptol.Prims.Syntax.ECon
instance GHC.Show.Show Cryptol.Prims.Syntax.ECon
instance GHC.Classes.Ord Cryptol.Prims.Syntax.ECon
instance GHC.Classes.Eq Cryptol.Prims.Syntax.ECon
instance GHC.Enum.Enum Cryptol.Prims.Syntax.TFun
instance GHC.Enum.Bounded Cryptol.Prims.Syntax.TFun
instance GHC.Classes.Ord Cryptol.Prims.Syntax.TFun
instance GHC.Classes.Eq Cryptol.Prims.Syntax.TFun
instance GHC.Show.Show Cryptol.Prims.Syntax.TFun
instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TFun
instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.ECon


module Cryptol.Parser.AST

-- | Module names are just namespaces.
--   
--   INVARIANT: the list of strings should never be empty in a valid module
--   name.
newtype ModName
ModName :: [String] -> ModName
modRange :: Module -> Range
data QName
QName :: (Maybe ModName) -> Name -> QName
mkQual :: ModName -> Name -> QName
mkUnqual :: Name -> QName
unqual :: QName -> Name
data Name
Name :: String -> Name
NewName :: Pass -> Int -> Name
data Named a
Named :: Located Name -> a -> Named a
[name] :: Named a -> Located Name
[value] :: Named a -> a
data Pass
NoPat :: Pass
MonoValues :: Pass
data Schema
Forall :: [TParam] -> [Prop] -> Type -> (Maybe Range) -> Schema
data TParam
TParam :: Name -> Maybe Kind -> Maybe Range -> TParam
[tpName] :: TParam -> Name
[tpKind] :: TParam -> Maybe Kind
[tpRange] :: TParam -> Maybe Range
tpQName :: TParam -> QName
data Kind
KNum :: Kind
KType :: Kind
data Type

-- | <pre>
--   [8] -&gt; [8]
--   </pre>
TFun :: Type -> Type -> Type

-- | <pre>
--   [8] a
--   </pre>
TSeq :: Type -> Type -> Type

-- | <pre>
--   Bit
--   </pre>
TBit :: Type

-- | <pre>
--   10
--   </pre>
TNum :: Integer -> Type

-- | <pre>
--   <tt>a</tt>
--   </pre>
TChar :: Char -> Type

-- | <pre>
--   inf
--   </pre>
TInf :: Type

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

-- | <pre>
--   2 + x
--   </pre>
TApp :: TFun -> [Type] -> Type

-- | <pre>
--   { x : [8], y : [32] }
--   </pre>
TRecord :: [Named Type] -> Type

-- | <pre>
--   ([8], [32])
--   </pre>
TTuple :: [Type] -> Type

-- | <tt>_</tt>, just some type.
TWild :: Type

-- | Location information
TLocated :: Type -> Range -> Type
data Prop

-- | <pre>
--   fin x
--   </pre>
CFin :: Type -> Prop

-- | <pre>
--   x == 10
--   </pre>
CEqual :: Type -> Type -> Prop

-- | <pre>
--   x &gt;= 10
--   </pre>
CGeq :: Type -> Type -> Prop

-- | <pre>
--   Arith a
--   </pre>
CArith :: Type -> Prop

-- | <pre>
--   Cmp a
--   </pre>
CCmp :: Type -> Prop

-- | Location information
CLocated :: Prop -> Range -> Prop
data Module
Module :: Located ModName -> [Located Import] -> [TopDecl] -> Module
[mName] :: Module -> Located ModName
[mImports] :: Module -> [Located Import]
[mDecls] :: Module -> [TopDecl]
newtype Program
Program :: [TopDecl] -> Program
data TopDecl
Decl :: (TopLevel Decl) -> TopDecl
TDNewtype :: (TopLevel Newtype) -> TopDecl
Include :: (Located FilePath) -> TopDecl
data Decl
DSignature :: [LQName] -> Schema -> Decl
DPragma :: [LQName] -> Pragma -> Decl
DBind :: Bind -> Decl
DPatBind :: Pattern -> Expr -> Decl
DType :: TySyn -> Decl
DLocated :: Decl -> Range -> Decl
data TySyn
TySyn :: LQName -> [TParam] -> Type -> TySyn

-- | Bindings. Notes:
--   
--   <ul>
--   <li>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.</li>
--   <li>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.</li>
--   </ul>
data Bind
Bind :: LQName -> [Pattern] -> Expr -> Maybe Schema -> [Pragma] -> Bool -> Bind

-- | Defined thing
[bName] :: Bind -> LQName

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

-- | Definition
[bDef] :: Bind -> Expr

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

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

-- | Is this a monomorphic binding
[bMono] :: Bind -> Bool
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma

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

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

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

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

-- | Check to see if a type synonym is exported.
isExportedType :: QName -> ExportSpec -> Bool
data TopLevel a
TopLevel :: ExportType -> a -> TopLevel a
[tlExport] :: TopLevel a -> ExportType
[tlValue] :: TopLevel a -> a

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

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

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

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

-- | Constructor
[nBody] :: Newtype -> [Named Type]

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

-- | <pre>
--   x
--   </pre>
EVar :: QName -> Expr

-- | <pre>
--   split
--   </pre>
ECon :: ECon -> Expr

-- | <pre>
--   0x10
--   </pre>
ELit :: Literal -> Expr

-- | <pre>
--   (1,2,3)
--   </pre>
ETuple :: [Expr] -> Expr

-- | <pre>
--   { x = 1, y = 2 }
--   </pre>
ERecord :: [Named Expr] -> Expr

-- | <pre>
--   e.l
--   </pre>
ESel :: Expr -> Selector -> Expr

-- | <pre>
--   [1,2,3]
--   </pre>
EList :: [Expr] -> Expr

-- | <pre>
--   [1, 5 ..  117 ]
--   </pre>
EFromTo :: Type -> (Maybe Type) -> (Maybe Type) -> Expr

-- | <pre>
--   [1, 3 ...]
--   </pre>
EInfFrom :: Expr -> (Maybe Expr) -> Expr

-- | <pre>
--   [ 1 | x &lt;- xs ]
--   </pre>
EComp :: Expr -> [[Match]] -> Expr

-- | <pre>
--   f x
--   </pre>
EApp :: Expr -> Expr -> Expr

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

-- | <pre>
--   if ok then e1 else e2
--   </pre>
EIf :: Expr -> Expr -> Expr -> Expr

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

-- | <pre>
--   1 : [8]
--   </pre>
ETyped :: Expr -> Type -> Expr

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

-- | <pre>
--   \x y -&gt; x
--   </pre>
EFun :: [Pattern] -> Expr -> Expr

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

-- | Literals.
data Literal

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

-- | <pre>
--   "hello"
--   </pre>
ECString :: String -> Literal

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

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

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

-- | overloaded decimal literal
DecLit :: NumInfo

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

-- | character literal
CharLit :: NumInfo

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

-- | p &lt;- e
Match :: Pattern -> Expr -> Match
MatchLet :: Bind -> Match
data Pattern

-- | <pre>
--   x
--   </pre>
PVar :: LName -> Pattern

-- | <pre>
--   _
--   </pre>
PWild :: Pattern

-- | <pre>
--   (x,y,z)
--   </pre>
PTuple :: [Pattern] -> Pattern

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

-- | <pre>
--   [ x, y, z ]
--   </pre>
PList :: [Pattern] -> Pattern

-- | <pre>
--   x : [8]
--   </pre>
PTyped :: Pattern -> Type -> Pattern

-- | <pre>
--   (x # y)
--   </pre>
PSplit :: Pattern -> Pattern -> Pattern

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

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

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

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

-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> (Maybe Int) -> Selector
data TypeInst
NamedInst :: (Named Type) -> TypeInst
PosInst :: Type -> TypeInst
data Located a
Located :: !Range -> a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> a

-- | A name with location information.
type LName = Located Name

-- | A qualified name with location information.
type LQName = Located QName

-- | A string with location information.
type LString = Located String
class NoPos t
noPos :: NoPos t => t -> t

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

-- | Display the thing selected by the selector, nicely.
ppSelector :: Selector -> Doc
instance GHC.Show.Show Cryptol.Parser.AST.Program
instance GHC.Classes.Eq Cryptol.Parser.AST.Program
instance GHC.Show.Show Cryptol.Parser.AST.Module
instance GHC.Classes.Eq Cryptol.Parser.AST.Module
instance GHC.Show.Show Cryptol.Parser.AST.TopDecl
instance GHC.Classes.Eq Cryptol.Parser.AST.TopDecl
instance GHC.Show.Show Cryptol.Parser.AST.ReplInput
instance GHC.Classes.Eq Cryptol.Parser.AST.ReplInput
instance GHC.Show.Show Cryptol.Parser.AST.Bind
instance GHC.Classes.Eq Cryptol.Parser.AST.Bind
instance GHC.Show.Show Cryptol.Parser.AST.Match
instance GHC.Classes.Eq Cryptol.Parser.AST.Match
instance GHC.Show.Show Cryptol.Parser.AST.Expr
instance GHC.Classes.Eq Cryptol.Parser.AST.Expr
instance GHC.Show.Show Cryptol.Parser.AST.Decl
instance GHC.Classes.Eq Cryptol.Parser.AST.Decl
instance GHC.Show.Show Cryptol.Parser.AST.Schema
instance GHC.Classes.Eq Cryptol.Parser.AST.Schema
instance GHC.Show.Show Cryptol.Parser.AST.Prop
instance GHC.Classes.Eq Cryptol.Parser.AST.Prop
instance GHC.Show.Show Cryptol.Parser.AST.TySyn
instance GHC.Classes.Eq Cryptol.Parser.AST.TySyn
instance GHC.Show.Show Cryptol.Parser.AST.Newtype
instance GHC.Classes.Eq Cryptol.Parser.AST.Newtype
instance GHC.Show.Show Cryptol.Parser.AST.TypeInst
instance GHC.Classes.Eq Cryptol.Parser.AST.TypeInst
instance GHC.Show.Show Cryptol.Parser.AST.Pattern
instance GHC.Classes.Eq Cryptol.Parser.AST.Pattern
instance GHC.Show.Show Cryptol.Parser.AST.Type
instance GHC.Classes.Eq Cryptol.Parser.AST.Type
instance GHC.Show.Show Cryptol.Parser.AST.TParam
instance GHC.Classes.Eq Cryptol.Parser.AST.TParam
instance GHC.Show.Show Cryptol.Parser.AST.Kind
instance GHC.Classes.Eq Cryptol.Parser.AST.Kind
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.Named a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.Named a)
instance GHC.Classes.Ord Cryptol.Parser.AST.Selector
instance GHC.Show.Show Cryptol.Parser.AST.Selector
instance GHC.Classes.Eq Cryptol.Parser.AST.Selector
instance GHC.Show.Show Cryptol.Parser.AST.Literal
instance GHC.Classes.Eq Cryptol.Parser.AST.Literal
instance GHC.Show.Show Cryptol.Parser.AST.NumInfo
instance GHC.Classes.Eq Cryptol.Parser.AST.NumInfo
instance GHC.Show.Show Cryptol.Parser.AST.ExportSpec
instance GHC.Classes.Ord a => GHC.Classes.Ord (Cryptol.Parser.AST.TopLevel a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.TopLevel a)
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.TopLevel a)
instance GHC.Classes.Ord Cryptol.Parser.AST.ExportType
instance GHC.Show.Show Cryptol.Parser.AST.ExportType
instance GHC.Classes.Eq Cryptol.Parser.AST.ExportType
instance GHC.Show.Show Cryptol.Parser.AST.Pragma
instance GHC.Classes.Eq Cryptol.Parser.AST.Pragma
instance GHC.Show.Show Cryptol.Parser.AST.Import
instance GHC.Classes.Eq Cryptol.Parser.AST.Import
instance GHC.Show.Show Cryptol.Parser.AST.ImportSpec
instance GHC.Classes.Eq Cryptol.Parser.AST.ImportSpec
instance GHC.Show.Show Cryptol.Parser.AST.QName
instance GHC.Classes.Ord Cryptol.Parser.AST.QName
instance GHC.Classes.Eq Cryptol.Parser.AST.QName
instance GHC.Show.Show Cryptol.Parser.AST.Name
instance GHC.Classes.Ord Cryptol.Parser.AST.Name
instance GHC.Classes.Eq Cryptol.Parser.AST.Name
instance GHC.Show.Show Cryptol.Parser.AST.Pass
instance GHC.Classes.Ord Cryptol.Parser.AST.Pass
instance GHC.Classes.Eq Cryptol.Parser.AST.Pass
instance GHC.Show.Show Cryptol.Parser.AST.ModName
instance GHC.Classes.Ord Cryptol.Parser.AST.ModName
instance GHC.Classes.Eq Cryptol.Parser.AST.ModName
instance GHC.Base.Functor Cryptol.Parser.AST.TopLevel
instance GHC.Base.Monoid Cryptol.Parser.AST.ExportSpec
instance GHC.Base.Functor Cryptol.Parser.AST.Named
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Expr
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Expr
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.TParam
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.TParam
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Type
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Type
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Prop
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Prop
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Pattern
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Pattern
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Bind
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Match
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Named a)
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Schema
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Schema
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Decl
instance Cryptol.Parser.Position.AddLoc Cryptol.Parser.AST.Decl
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.TopDecl
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Module
instance Cryptol.Parser.Position.HasLoc Cryptol.Parser.AST.Newtype
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Module
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Program
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TopDecl
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Decl
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Newtype
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Import
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ImportSpec
instance Cryptol.Utils.PP.PP a => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pragma
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Bind
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TySyn
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.ModName
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.QName
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Name
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Literal
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TypeInst
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Expr
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Selector
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Pattern
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Match
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Schema
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Kind
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.TParam
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Type
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Prop
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.Position.Located t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Named t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos [t]
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (GHC.Base.Maybe t)
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Program
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Module
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TopDecl
instance Cryptol.Parser.AST.NoPos a => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Decl
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Newtype
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Bind
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pragma
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TySyn
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Expr
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TypeInst
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Match
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pattern
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Schema
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.TParam
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Type
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Prop


module Cryptol.TypeCheck.AST

-- | A Cryptol module.
data Module
Module :: ModName -> ExportSpec -> [Import] -> Map QName TySyn -> Map QName Newtype -> [DeclGroup] -> Module
[mName] :: Module -> ModName
[mExports] :: Module -> ExportSpec
[mImports] :: Module -> [Import]
[mTySyns] :: Module -> Map QName TySyn
[mNewtypes] :: Module -> Map QName Newtype
[mDecls] :: Module -> [DeclGroup]

-- | Kinds, classify types.
data Kind
KType :: Kind
KNum :: Kind
KProp :: Kind
(:->) :: Kind -> Kind -> Kind

-- | The types of polymorphic values.
data Schema
Forall :: [TParam] -> [Prop] -> Type -> Schema
[sVars] :: Schema -> [TParam]
[sProps] :: Schema -> [Prop]
[sType] :: Schema -> Type

-- | Type synonym.
data TySyn
TySyn :: QName -> [TParam] -> [Prop] -> Type -> TySyn

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

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

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

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

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

-- | Type parameters.
data TParam
TParam :: !Int -> Kind -> Maybe QName -> TParam

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

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

-- | Name from source, if any.
[tpName] :: TParam -> Maybe QName
tpVar :: TParam -> TVar

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

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

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

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

-- | Record type
TRec :: [(Name, Type)] -> Type

-- | The type is supposed to be of kind <a>KProp</a>
type Prop = Type

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

-- | Type variables.
data TVar

-- | Unique, kind, ids of bound type variables that are in scope The
--   <a>Doc</a> is a description of how this type came to be.
TVFree :: !Int -> Kind -> (Set TVar) -> Doc -> TVar
TVBound :: !Int -> Kind -> TVar

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

-- | Built-in type constants.
--   
--   Predicate symbols.
data PC

-- | <pre>
--   _ == _
--   </pre>
PEqual :: PC

-- | <pre>
--   _ /= _
--   </pre>
PNeq :: PC

-- | <pre>
--   _ &gt;= _
--   </pre>
PGeq :: PC

-- | <pre>
--   fin _
--   </pre>
PFin :: PC

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

-- | <pre>
--   Arith _
--   </pre>
PArith :: PC

-- | <pre>
--   Cmp _
--   </pre>
PCmp :: PC

-- | 1-1 constants.
data TC

-- | Numbers
TCNum :: Integer -> TC

-- | Inf
TCInf :: TC

-- | Bit
TCBit :: TC

-- | <pre>
--   [_] _
--   </pre>
TCSeq :: TC

-- | <pre>
--   _ -&gt; _
--   </pre>
TCFun :: TC

-- | <pre>
--   (_, _, _)
--   </pre>
TCTuple :: Int -> TC

-- | user-defined, <tt>T</tt>
TCNewtype :: UserTC -> TC
data UserTC
UserTC :: QName -> Kind -> UserTC
data Expr

-- | Built-in constant
ECon :: ECon -> Expr

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

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

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

-- | Elimination for tuple<i>record</i>list
ESel :: Expr -> Selector -> Expr

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

-- | List comprehensions The type caches the type of the expr.
EComp :: Type -> Expr -> [[Match]] -> Expr

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

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

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

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

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

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

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

-- | if e : t1, then cast e : t2 as long as we can prove that 't1 = t2'. We
--   could express this in terms of a built-in constant. `cast :: {a,b} (a
--   =*= b) =&gt; a -&gt; b`
--   
--   Using the constant is a bit verbose though, because we end up with
--   both the source and target type. So, instead we use this language
--   construct, which only stores the target type, and the source type can
--   be reconstructed from the expression.
--   
--   Another way to think of this is simply as an expression with an
--   explicit type annotation.
ECast :: Expr -> Type -> Expr
EWhere :: Expr -> [DeclGroup] -> Expr
data Match

-- | do we need this type? it seems like it can be computed from the expr
From :: QName -> Type -> Expr -> Match
Let :: Decl -> Match
data DeclGroup

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

-- | Non-recursive declaration
NonRecursive :: Decl -> DeclGroup
groupDecls :: DeclGroup -> [Decl]
data Decl
Decl :: QName -> Schema -> Expr -> [Pragma] -> Decl
[dName] :: Decl -> QName
[dSignature] :: Decl -> Schema
[dDefinition] :: Decl -> Expr
[dPragmas] :: Decl -> [Pragma]
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsNum :: Type -> Maybe Integer
tIsInf :: Type -> Bool
tIsVar :: Type -> Maybe TVar
tIsFun :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsBit :: Type -> Bool
tIsTuple :: Type -> Maybe [Type]
pIsFin :: Prop -> Maybe Type
pIsGeq :: Prop -> Maybe (Type, Type)
pIsEq :: Prop -> Maybe (Type, Type)
pIsArith :: Prop -> Maybe Type
pIsCmp :: Prop -> Maybe Type
pIsNumeric :: Prop -> Bool
tNum :: Integral a => a -> Type
tZero :: Type
tOne :: Type
tTwo :: Type
tInf :: Type
tBit :: Type
eTrue :: Expr
eFalse :: Expr
tWord :: Type -> Type
tSeq :: Type -> Type -> Type
tChar :: Type
eChar :: Char -> Expr
tString :: Int -> Type
eString :: String -> Expr

-- | Make an expression that is <a>error</a> pre-applied to a type and a
--   message.
eError :: Type -> String -> Expr
tRec :: [(Name, Type)] -> Type
tTuple :: [Type] -> Type

-- | Make a function type.
tFun :: Type -> Type -> Type

-- | Eliminate type synonyms.
tNoUser :: Type -> Type
tWidth :: Type -> Type
tLenFromThen :: Type -> Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
tMax :: Type -> Type -> Type

-- | Equality for numeric types.
(=#=) :: Type -> Type -> Prop
(=/=) :: Type -> Type -> Prop
pArith :: Type -> Prop
pCmp :: Type -> Prop

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

-- | A <tt>Has</tt> constraint, used for tuple and record selection.
pHas :: Selector -> Type -> Type -> Prop
pFin :: Type -> Prop

-- | Make multiplication type.
(.*.) :: Type -> Type -> Type

-- | Make addition type.
(.+.) :: Type -> Type -> Type
(.-.) :: Type -> Type -> Type
(.^.) :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type

-- | Make a <tt>min</tt> type.
tMin :: Type -> Type -> Type
newtypeTyCon :: Newtype -> TCon
newtypeConType :: Newtype -> Schema
class HasKind t
kindOf :: HasKind t => t -> Kind
quickApply :: Kind -> [a] -> Kind
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(QName, Type)] -> Expr -> Doc
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitAbs :: Expr -> Maybe ((QName, Type), Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)

-- | Built-in types.
data TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCAdd :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCSub :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMul :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCDiv :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMod :: TFun

-- | <pre>
--   : Num -&gt; Num
--   </pre>
TCLg2 :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCExp :: TFun

-- | <pre>
--   : Num -&gt; Num
--   </pre>
TCWidth :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMin :: TFun

-- | <pre>
--   : Num -&gt; Num -&gt; Num
--   </pre>
TCMax :: TFun

-- | <tt> : Num -&gt; Num -&gt; Num -&gt; Num</tt> Example: <tt>[ 1, 5 .. ]
--   :: [lengthFromThen 1 5 b][b]</tt>
TCLenFromThen :: TFun

-- | <tt> : Num -&gt; Num -&gt; Num -&gt; Num</tt> Example: <tt>[ 1, 5 .. 9
--   ] :: [lengthFromThenTo 1 5 9][b]</tt>
TCLenFromThenTo :: TFun
data Name
Name :: String -> Name
NewName :: Pass -> Int -> Name
data QName
QName :: (Maybe ModName) -> Name -> QName
mkUnqual :: Name -> QName
unqual :: QName -> Name

-- | Module names are just namespaces.
--   
--   INVARIANT: the list of strings should never be empty in a valid module
--   name.
newtype ModName
ModName :: [String] -> ModName

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

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

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

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

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

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

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

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

-- | Check to see if a type synonym is exported.
isExportedType :: QName -> ExportSpec -> Bool
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma
instance GHC.Show.Show Cryptol.TypeCheck.AST.Module
instance GHC.Show.Show Cryptol.TypeCheck.AST.Match
instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclGroup
instance GHC.Show.Show Cryptol.TypeCheck.AST.Expr
instance GHC.Show.Show Cryptol.TypeCheck.AST.Decl
instance GHC.Show.Show Cryptol.TypeCheck.AST.Schema
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Schema
instance GHC.Show.Show Cryptol.TypeCheck.AST.TySyn
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TySyn
instance GHC.Show.Show Cryptol.TypeCheck.AST.Newtype
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.Type
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Type
instance GHC.Show.Show Cryptol.TypeCheck.AST.Type
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TCon
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TCon
instance GHC.Show.Show Cryptol.TypeCheck.AST.TCon
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TC
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TC
instance GHC.Show.Show Cryptol.TypeCheck.AST.TC
instance GHC.Show.Show Cryptol.TypeCheck.AST.UserTC
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.PC
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.PC
instance GHC.Show.Show Cryptol.TypeCheck.AST.PC
instance GHC.Show.Show Cryptol.TypeCheck.AST.TVar
instance GHC.Show.Show Cryptol.TypeCheck.AST.TParam
instance GHC.Show.Show Cryptol.TypeCheck.AST.Kind
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Kind
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TParam
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TParam
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.UserTC
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.UserTC
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TVar
instance GHC.Classes.Ord Cryptol.TypeCheck.AST.TVar
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TVar
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TCon
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.UserTC
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TC
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.PC
instance Cryptol.TypeCheck.AST.HasKind Cryptol.Prims.Syntax.TFun
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.Type
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TySyn
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.Newtype
instance Cryptol.TypeCheck.AST.HasKind Cryptol.TypeCheck.AST.TParam
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Kind
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TVar)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TParam
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TParam)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Type)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Schema
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Schema)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TySyn
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.TySyn)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Type
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TCon
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.PC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.TC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.UserTC
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Expr)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Expr
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Match)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Match
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.DeclGroup)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Decl)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Decl
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.AST.Module
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.AST.Module)


module Cryptol.Prims.Types

-- | Types of built-in constants.
typeOf :: ECon -> Schema


module Cryptol.Prims.Doc
helpDoc :: ECon -> Doc
description :: ECon -> Doc


module Cryptol.Eval.Error

-- | Panic from an Eval context.
evalPanic :: String -> [String] -> a
data EvalError
InvalidIndex :: Integer -> EvalError
TypeCannotBeDemoted :: Type -> EvalError
DivideByZero :: EvalError
WordTooWide :: Integer -> EvalError
UserError :: String -> EvalError

-- | A sequencing operation has gotten an invalid index.
invalidIndex :: Integer -> a

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

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

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

-- | For <a>error</a>
cryUserError :: String -> a
instance GHC.Show.Show Cryptol.Eval.Error.EvalError
instance Cryptol.Utils.PP.PP Cryptol.Eval.Error.EvalError
instance GHC.Exception.Exception Cryptol.Eval.Error.EvalError


module Cryptol.Eval.Value
isTBit :: TValue -> Bool
isTSeq :: TValue -> Maybe (TValue, TValue)
isTFun :: TValue -> Maybe (TValue, TValue)
isTTuple :: TValue -> Maybe (Int, [TValue])
isTRec :: TValue -> Maybe [(Name, TValue)]
tvSeq :: TValue -> TValue -> TValue
numTValue :: TValue -> Nat'
toNumTValue :: Nat' -> TValue
finTValue :: TValue -> Integer
data BV

-- | width, value The value may contain junk bits
BV :: !Integer -> !Integer -> BV

-- | Smart constructor for <a>BV</a>s that checks for the width limit
mkBv :: Integer -> Integer -> BV

-- | Generic value type, parameterized by bit and word types.
data GenValue b w
VRecord :: [(Name, GenValue b w)] -> GenValue b w
VTuple :: [GenValue b w] -> GenValue b w
VBit :: b -> GenValue b w
VSeq :: Bool -> [GenValue b w] -> GenValue b w
VWord :: w -> GenValue b w
VStream :: [GenValue b w] -> GenValue b w
VFun :: (GenValue b w -> GenValue b w) -> GenValue b w
VPoly :: (TValue -> GenValue b w) -> GenValue b w
type Value = GenValue Bool BV

-- | An evaluated type. These types do not contain type variables, type
--   synonyms, or type functions.
newtype TValue
TValue :: Type -> TValue
[tValTy] :: TValue -> Type
data PPOpts
PPOpts :: Bool -> Int -> Int -> PPOpts
[useAscii] :: PPOpts -> Bool
[useBase] :: PPOpts -> Int
[useInfLength] :: PPOpts -> Int
defaultPPOpts :: PPOpts
ppValue :: PPOpts -> Value -> Doc
asciiMode :: PPOpts -> Integer -> Bool
integerToChar :: Integer -> Char
data WithBase a
WithBase :: PPOpts -> a -> WithBase a
ppWord :: PPOpts -> BV -> Doc
class BitWord b w

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

-- | NOTE this produces a list of bits that represent a big-endian word, so
--   the most significant bit is the first element of the list.
unpackWord :: BitWord b w => w -> [b]
mask :: Integer -> Integer -> Integer

-- | Create a packed word of n bits.
word :: Integer -> Integer -> Value
lam :: (GenValue b w -> GenValue b w) -> GenValue b w

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

-- | Generate a stream.
toStream :: [GenValue b w] -> GenValue b w
toFinSeq :: TValue -> [GenValue b w] -> GenValue b w

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

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

-- | Construct one of: * a word, when the sequence is finite and the
--   elements are bits * a sequence, when the sequence is finite but the
--   elements aren't bits * a stream, when the sequence is not finite
--   
--   NOTE: do not use this constructor in the case where the thing may be a
--   finite, but recursive, sequence.
toPackedSeq :: TValue -> TValue -> [Value] -> Value

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

-- | Extract a sequence.
fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
fromStr :: Value -> String

-- | Extract a packed word. Note that this does not clean-up any junk bits
--   in the word.
fromVWord :: BitWord b w => GenValue b w -> w
vWordLen :: Value -> Maybe Integer

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

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

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

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

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

-- | Lookup a field in a record.
lookupRecord :: Name -> GenValue b w -> GenValue b w

-- | Given an expected type, returns an expression that evaluates to this
--   value, if we can determine it.
--   
--   XXX: View patterns would probably clean up this definition a lot.
toExpr :: Type -> Value -> Maybe Expr
instance GHC.Base.Functor Cryptol.Eval.Value.WithBase
instance GHC.Show.Show Cryptol.Eval.Value.TValue
instance Cryptol.Utils.PP.PP (Cryptol.Eval.Value.WithBase Cryptol.Eval.Value.Value)
instance Cryptol.Eval.Value.BitWord GHC.Types.Bool Cryptol.Eval.Value.BV


-- | Evaluate test cases and handle exceptions appropriately
module Cryptol.Testing.Eval

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

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


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

-- | An evaluated type. These types do not contain type variables, type
--   synonyms, or type functions.
data TValue
numTValue :: TValue -> Nat'
toNumTValue :: Nat' -> TValue
finTValue :: TValue -> Integer
isTBit :: TValue -> Bool
isTFun :: TValue -> Maybe (TValue, TValue)
isTSeq :: TValue -> Maybe (TValue, TValue)
isTTuple :: TValue -> Maybe (Int, [TValue])
isTRec :: TValue -> Maybe [(Name, TValue)]
tvSeq :: TValue -> TValue -> TValue

-- | Generic value type, parameterized by bit and word types.
data GenValue b w
VRecord :: [(Name, GenValue b w)] -> GenValue b w
VTuple :: [GenValue b w] -> GenValue b w
VBit :: b -> GenValue b w
VSeq :: Bool -> [GenValue b w] -> GenValue b w
VWord :: w -> GenValue b w
VStream :: [GenValue b w] -> GenValue b w
VFun :: (GenValue b w -> GenValue b w) -> GenValue b w
VPoly :: (TValue -> GenValue b w) -> GenValue b w
lam :: (GenValue b w -> GenValue b w) -> GenValue b w

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

-- | Generate a stream.
toStream :: [GenValue b w] -> GenValue b w
toFinSeq :: TValue -> [GenValue b w] -> GenValue b w

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

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

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

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

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

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

-- | Lookup a field in a record.
lookupRecord :: Name -> GenValue b w -> GenValue b w

-- | Extract a sequence.
fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]

-- | Extract a packed word. Note that this does not clean-up any junk bits
--   in the word.
fromVWord :: BitWord b w => GenValue b w -> w
evalPanic :: String -> [String] -> a
iteValue :: SBool -> Value -> Value -> Value
mergeValue :: Bool -> SBool -> Value -> Value -> Value
instance Cryptol.Eval.Value.BitWord Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord


-- | This module generates random values for Cryptol types.
module Cryptol.Testing.Random
type Gen g = Int -> g -> (Value, g)

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

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

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

-- | Generate a random bit value.
randomBit :: RandomGen g => Gen g

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

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

-- | Generate a random sequence. Generally, this should be used for
--   sequences other than bits. For sequences of bits use "randomWord". The
--   difference is mostly about how the results will be displayed.
randomSequence :: RandomGen g => Integer -> Gen g -> Gen g

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

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


module Cryptol.Eval.Env
type ReadEnv = EvalEnv
data EvalEnv
EvalEnv :: Map QName Value -> Map TVar TValue -> EvalEnv
[envVars] :: EvalEnv -> Map QName Value
[envTypes] :: EvalEnv -> Map TVar TValue
emptyEnv :: EvalEnv

-- | Bind a variable in the evaluation environment.
bindVar :: QName -> Value -> EvalEnv -> EvalEnv

-- | Lookup a variable in the environment.
lookupVar :: QName -> EvalEnv -> Maybe Value

-- | Bind a type variable of kind *.
bindType :: TVar -> TValue -> EvalEnv -> EvalEnv

-- | Lookup a type variable.
lookupType :: TVar -> EvalEnv -> Maybe TValue
instance GHC.Base.Monoid Cryptol.Eval.Env.EvalEnv
instance Cryptol.Utils.PP.PP (Cryptol.Eval.Value.WithBase Cryptol.Eval.Env.EvalEnv)


module Cryptol.Eval.Type

-- | Evaluation for types.
evalType :: EvalEnv -> Type -> TValue

-- | Reduce type functions, rising an exception for undefined values.
evalTF :: TFun -> [TValue] -> TValue


module Cryptol.Prims.Eval
evalECon :: ECon -> Value

-- | Make a numeric constant.
ecDemoteV :: Value
divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)

-- | Create a packed word
modExp :: Integer -> Integer -> Integer -> Integer
doubleAndAdd :: Integer -> Integer -> Integer -> Integer
type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w
type Binary = GenBinary Bool BV
binary :: GenBinary b w -> GenValue b w
type GenUnary b w = TValue -> GenValue b w -> GenValue b w
type Unary = GenUnary Bool BV
unary :: GenUnary b w -> GenValue b w

-- | Turn a normal binop on Integers into one that can also deal with a
--   bitsize.
liftBinArith :: (Integer -> Integer -> Integer) -> BinArith
type BinArith = Integer -> Integer -> Integer -> Integer
arithBinary :: BinArith -> Binary
arithUnary :: (Integer -> Integer) -> Unary
lg2 :: Integer -> Integer
divWrap :: Integral a => a -> a -> a
modWrap :: Integral a => a -> a -> a

-- | Lexicographic ordering on two values.
lexCompare :: TValue -> Value -> Value -> Ordering
zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering

-- | Process two elements based on their lexicographic ordering.
cmpOrder :: (Ordering -> Bool) -> Binary
withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary
maxV :: Ordering -> TValue -> Value -> Value -> Value
minV :: Ordering -> TValue -> Value -> Value -> Value
funCmp :: (Ordering -> Bool) -> Value
zeroV :: TValue -> Value

-- | Join a sequence of sequences into a single sequence.
joinV :: TValue -> TValue -> TValue -> Value -> Value
splitAtV :: TValue -> TValue -> TValue -> Value -> Value

-- | Split implementation.
ecSplitV :: Value

-- | Split into infinitely many chunks
infChunksOf :: Integer -> [a] -> [[a]]

-- | Split into finitely many chunks
finChunksOf :: Integer -> Integer -> [a] -> [[a]]
ccatV :: TValue -> TValue -> TValue -> Value -> Value -> Value

-- | Merge two values given a binop. This is used for and, or and xor.
logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary
logicUnary :: (forall a. Bits a => a -> a) -> Unary
logicShift :: (Integer -> Integer -> Int -> Integer) -> (TValue -> TValue -> [Value] -> Int -> [Value]) -> Value
shiftLW :: Integer -> Integer -> Int -> Integer
shiftLS :: TValue -> TValue -> [Value] -> Int -> [Value]
shiftRW :: Integer -> Integer -> Int -> Integer
shiftRS :: TValue -> TValue -> [Value] -> Int -> [Value]
rotateLW :: Integer -> Integer -> Int -> Integer
rotateLS :: TValue -> TValue -> [Value] -> Int -> [Value]
rotateRW :: Integer -> Integer -> Int -> Integer
rotateRS :: TValue -> TValue -> [Value] -> Int -> [Value]

-- | Indexing operations that return one element.
indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value
indexFront :: Maybe Integer -> [Value] -> Integer -> Value
indexBack :: Maybe Integer -> [Value] -> Integer -> Value

-- | Indexing operations that return many elements.
indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value
indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
fromThenV :: Value
fromToV :: Value
fromThenToV :: Value

-- | Produce a random value with the given seed. If we do not support
--   making values of the given type, return zero of that type. TODO: do
--   better than returning zero
randomV :: TValue -> Integer -> Value
tlamN :: (Nat' -> GenValue b w) -> GenValue b w


module Cryptol.Eval
moduleEnv :: Module -> EvalEnv -> EvalEnv
data EvalEnv
emptyEnv :: EvalEnv
evalExpr :: EvalEnv -> Expr -> Value
evalDecls :: [DeclGroup] -> EvalEnv -> EvalEnv
data EvalError
InvalidIndex :: Integer -> EvalError
TypeCannotBeDemoted :: Type -> EvalError
DivideByZero :: EvalError
WordTooWide :: Integer -> EvalError
UserError :: String -> EvalError
data WithBase a
WithBase :: PPOpts -> a -> WithBase a


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


module Cryptol.TypeCheck.Subst
data Subst
S :: Map TVar Type -> !Bool -> Subst
[suMap] :: Subst -> Map TVar Type
[suDefaulting] :: Subst -> !Bool
emptySubst :: Subst
singleSubst :: TVar -> Type -> Subst
(@@) :: Subst -> Subst -> Subst
defaultingSubst :: Subst -> Subst

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

-- | Pick types for unconstrained unification variables.
defaultFreeVar :: TVar -> Type

-- | Apply the substitution to the keys of a type map.
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a

-- | WARNING: This instance assumes that the quantified variables in the
--   types in the substitution will not get captured by the quantified
--   variables. This is reasonable because there should be no shadowing of
--   quantified variables but, just in case, we make a sanity check and
--   panic if somehow capture did occur.
instance GHC.Show.Show Cryptol.TypeCheck.Subst.Subst
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Subst.Subst)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Subst.Subst
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.AST.Type
instance Cryptol.TypeCheck.Subst.FVS a => Cryptol.TypeCheck.Subst.FVS [a]
instance (Cryptol.TypeCheck.Subst.FVS a, Cryptol.TypeCheck.Subst.FVS b) => Cryptol.TypeCheck.Subst.FVS (a, b)
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.AST.Schema
instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars (GHC.Base.Maybe t)
instance Cryptol.TypeCheck.Subst.TVars t => Cryptol.TypeCheck.Subst.TVars [t]
instance (Cryptol.TypeCheck.Subst.TVars s, Cryptol.TypeCheck.Subst.TVars t) => Cryptol.TypeCheck.Subst.TVars (s, t)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Type
instance (GHC.Base.Functor m, Cryptol.TypeCheck.Subst.TVars a) => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.List m a)
instance Cryptol.TypeCheck.Subst.TVars a => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.TypeMap a)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Schema
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Expr
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Match
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Decl
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module


module Cryptol.TypeCheck.Unify

-- | The most general unifier is a substitution and a set of constraints on
--   bound variables.
type MGU = (Subst, [Prop])
data Result a
OK :: a -> Result a
Error :: UnificationError -> Result a
data UnificationError
UniTypeMismatch :: Type -> Type -> UnificationError
UniKindMismatch :: Kind -> Kind -> UnificationError
UniTypeLenMismatch :: Int -> Int -> UnificationError
UniRecursive :: TVar -> Type -> UnificationError
UniNonPolyDepends :: TVar -> [TVar] -> UnificationError
UniNonPoly :: TVar -> Type -> UnificationError
uniError :: UnificationError -> Result a
emptyMGU :: MGU
mgu :: Type -> Type -> Result MGU
mguMany :: [Type] -> [Type] -> Result MGU
bindVar :: TVar -> Type -> Result MGU
instance GHC.Base.Functor Cryptol.TypeCheck.Unify.Result
instance GHC.Base.Applicative Cryptol.TypeCheck.Unify.Result
instance GHC.Base.Monad Cryptol.TypeCheck.Unify.Result


module Cryptol.TypeCheck.TypeOf

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


module Cryptol.TypeCheck.Solver.Utils
splitMins :: Type -> [Type]

-- | All ways to split a type in the form: `a + t1`, where <tt>a</tt> 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 <tt>k</tt>
--   is a constant &gt; 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 <tt>k</tt>
--   is a constant &gt; 1 This assumes that the type has been simplified
--   already, so that constants are floated to the left.
splitConstFactor :: Type -> Maybe (Integer, Type)


module Cryptol.Testing.Exhaust

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

-- | Apply a testable value to some arguments. Please note that this
--   function assumes that the values come from a call to
--   <a>testableType</a> (i.e., things are type-correct)
runOneTest :: Value -> [Value] -> IO TestResult

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

-- | Returns all the values in a type. Returns an empty list of values, for
--   types where <a>typeSize</a> returned <a>Nothing</a>.
typeValues :: Type -> [Value]


-- | This module defines the scoping rules for value- and type-level names
--   in Cryptol.
module Cryptol.Parser.Names
modExports :: Module -> ExportSpec

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

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

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

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

-- | The names defined and used by a single binding.
namesB :: Bind -> ([Located QName], Set QName)

-- | The names used by an expression.
namesE :: Expr -> Set QName

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

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

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

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

-- | Remove some defined variables from a set of free variables.
boundNames :: [Located QName] -> Set QName -> Set QName

-- | Given the set of type variables that are in scope, compute the type
--   synonyms used by a type.
namesT :: Set QName -> Type -> Set QName

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

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

-- | The type names used by a single binding.
tnamesB :: Bind -> Set QName

-- | The type names used by an expression.
tnamesE :: Expr -> Set QName
tnamesTI :: TypeInst -> Set QName

-- | The type names used by a pattern.
tnamesP :: Pattern -> Set QName

-- | The type names used by a match.
tnamesM :: Match -> Set QName

-- | The type names used by a type schema.
tnamesS :: Schema -> Set QName

-- | The type names used by a prop.
tnamesC :: Prop -> Set QName

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


module Cryptol.ModuleSystem.Interface

-- | The resulting interface generated by a module that has been
--   typechecked.
data Iface
Iface :: ModName -> IfaceDecls -> IfaceDecls -> Iface
[ifModName] :: Iface -> ModName
[ifPublic] :: Iface -> IfaceDecls
[ifPrivate] :: Iface -> IfaceDecls
data IfaceDecls
IfaceDecls :: Map QName [IfaceTySyn] -> Map QName [IfaceNewtype] -> Map QName [IfaceDecl] -> IfaceDecls
[ifTySyns] :: IfaceDecls -> Map QName [IfaceTySyn]
[ifNewtypes] :: IfaceDecls -> Map QName [IfaceNewtype]
[ifDecls] :: IfaceDecls -> Map QName [IfaceDecl]
type IfaceTySyn = TySyn
ifTySynName :: TySyn -> QName
type IfaceNewtype = Newtype
data IfaceDecl
IfaceDecl :: QName -> Schema -> [Pragma] -> IfaceDecl
[ifDeclName] :: IfaceDecl -> QName
[ifDeclSig] :: IfaceDecl -> Schema
[ifDeclPragmas] :: IfaceDecl -> [Pragma]
mkIfaceDecl :: Decl -> IfaceDecl

-- | Like mappend for IfaceDecls, but preferring entries on the left.
shadowing :: IfaceDecls -> IfaceDecls -> IfaceDecls

-- | Interpret an import declaration in the scope of the interface it
--   targets.
interpImport :: Import -> Iface -> Iface
unqualified :: IfaceDecls -> IfaceDecls

-- | Generate an Iface from a typechecked module.
genIface :: Module -> Iface
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.Iface
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecl
instance GHC.Base.Monoid Cryptol.ModuleSystem.Interface.IfaceDecls


-- | This module implements a transformation, which tries to avoid
--   exponential slow down in some cases. What's the problem? Consider the
--   following (common) patterns:
--   
--   fibs = [0,1] # [ x + y | x &lt;- fibs, y &lt;- drop`{1} fibs ]
--   
--   The type of <tt>fibs</tt> is:
--   
--   {a} (a &gt;= 1, fin a) =&gt; [inf][a]
--   
--   Here <tt>a</tt> is the number of bits to be used in the values
--   computed by <tt>fibs</tt>. When we evaluate <tt>fibs</tt>, <tt>a</tt>
--   becomes a parameter to <tt>fibs</tt>, which works except that now
--   <tt>fibs</tt> 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
--   <tt>fibs</tt> 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 <tt>fibs</tt>: each
--   recursive call to <tt>fibs</tt> is instantiated with exactly the same
--   type parameter (i.e., <tt>a</tt>). The rewrite we do is as follows:
--   
--   fibs : {a} (a &gt;= 1, fin a) =&gt; [inf][a] fibs = {a} (a &gt;= 1,
--   fin a) -&gt; fibs' where fibs' : [inf][a] fibs' = [0,1] # [ x + y | x
--   &lt;- fibs', y &lt;- drop`{1} fibs' ]
--   
--   After the rewrite, the recursion is monomorphic (i.e., we are always
--   using the same type). As a result, <tt>fibs'</tt> 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 &gt;= 2, fin a) =&gt; [inf][a] zig = [1] # zag
--   
--   zag : {a} (a &gt;= 2, fin a) =&gt; [inf][a] zag = [2] # zig
--   
--   This gets rewritten to:
--   
--   newName : {a} (a &gt;= 2, fin a) =&gt; ([inf][a], [inf][a]) newName =
--   {a} (a &gt;= 2, fin a) -&gt; (zig', zag') where zig' : [inf][a] zig' =
--   [1] # zag'
--   
--   zag' : [inf][a] zag' = [2] # zig'
--   
--   zig : {a} (a &gt;= 2, fin a) =&gt; [inf][a] zig = {a} (a &gt;= 2, fin
--   a) -&gt; (newName a &lt;&gt; &lt;&gt; ).1
--   
--   zag : {a} (a &gt;= 2, fin a) =&gt; [inf][a] zag = {a} (a &gt;= 2, fin
--   a) -&gt; (newName a &lt;&gt; &lt;&gt; ).2
--   
--   NOTE: We are assuming that no capture would occur with binders. For
--   values, this is because we replaces things with freshly chosen
--   variables. For types, this should be because there should be no
--   shadowing in the types. XXX: Make sure that this really is the case
--   for types!!
module Cryptol.Transform.MonoValues

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


module Cryptol.ModuleSystem.NamingEnv
data NameOrigin
Local :: (Located QName) -> NameOrigin
Imported :: QName -> NameOrigin
data EName
EFromBind :: (Located QName) -> EName
EFromNewtype :: (Located QName) -> EName
EFromMod :: QName -> EName
data TName
TFromParam :: QName -> TName
TFromSyn :: (Located QName) -> TName
TFromNewtype :: (Located QName) -> TName
TFromMod :: QName -> TName
class HasQName a
qname :: HasQName a => a -> QName
origin :: HasQName a => a -> NameOrigin
data NamingEnv
NamingEnv :: Map QName [EName] -> Map QName [TName] -> NamingEnv

-- | Expr renaming environment
[neExprs] :: NamingEnv -> Map QName [EName]

-- | Type renaming environment
[neTypes] :: NamingEnv -> Map QName [TName]

-- | Singleton type renaming environment.
singletonT :: QName -> TName -> NamingEnv

-- | Singleton expression renaming environment.
singletonE :: QName -> EName -> NamingEnv

-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
travNamingEnv :: Applicative f => (QName -> f QName) -> NamingEnv -> f NamingEnv

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

-- | Generate a type renaming environment from the parameters that are
--   bound by this schema.

-- | Produce a naming environment from an interface file, that contains a
--   mapping only from unqualified names to qualified ones.

-- | Translate a set of declarations from an interface into a naming
--   environment.

-- | Translate names bound by the patterns of a match into a renaming
--   environment.

-- | Generate the naming environment for a type parameter.

-- | Generate an expression renaming environment from a pattern. This
--   ignores type parameters that can be bound by the pattern.

-- | The naming environment for a single module. This is the mapping from
--   unqualified internal names to fully qualified names.

-- | The naming environment for a single declaration, unqualified. This is
--   meanat to be used for things like where clauses.
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.TName
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.EName
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NameOrigin
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.NamingEnv.NameOrigin
instance Cryptol.ModuleSystem.NamingEnv.HasQName Cryptol.ModuleSystem.NamingEnv.TName
instance Cryptol.ModuleSystem.NamingEnv.HasQName Cryptol.ModuleSystem.NamingEnv.EName
instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames (GHC.Base.Maybe a)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames [a]
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Schema
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.Interface.Iface
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.Interface.IfaceDecls
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Match
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Bind
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.TParam
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Pattern
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Module
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.Parser.AST.Decl


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

-- | Eliminate all patterns in a program.
removePatterns :: RemovePatterns t => t -> (t, [Error])
data Error
MultipleSignatures :: QName -> [Located Schema] -> Error
SignatureNoBind :: (Located QName) -> Schema -> Error
PragmaNoBind :: (Located QName) -> Pragma -> Error
instance GHC.Show.Show Cryptol.Parser.NoPat.Error
instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Program
instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Expr
instance Cryptol.Parser.NoPat.RemovePatterns Cryptol.Parser.AST.Module
instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl]
instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM
instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error


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

module Cryptol.Parser
parseModule :: Config -> String -> Either ParseError Module
parseProgram :: Layout -> String -> Either ParseError Program
parseProgramWith :: Config -> String -> Either ParseError Program
parseExpr :: String -> Either ParseError Expr
parseExprWith :: Config -> String -> Either ParseError Expr
parseDecl :: String -> Either ParseError Decl
parseDeclWith :: Config -> String -> Either ParseError Decl
parseDecls :: String -> Either ParseError [Decl]
parseDeclsWith :: Config -> String -> Either ParseError [Decl]
parseLetDecl :: String -> Either ParseError Decl
parseLetDeclWith :: Config -> String -> Either ParseError Decl
parseRepl :: String -> Either ParseError ReplInput
parseReplWith :: Config -> String -> Either ParseError ReplInput
parseSchema :: String -> Either ParseError Schema
parseSchemaWith :: Config -> String -> Either ParseError Schema
parseModName :: String -> Maybe ModName
data ParseError
HappyError :: FilePath -> Position -> (Maybe Token) -> ParseError
HappyErrorMsg :: Range -> String -> ParseError
ppError :: ParseError -> Doc
data Layout
Layout :: Layout
NoLayout :: Layout
data Config
Config :: !FilePath -> !Layout -> PreProc -> [FilePath] -> Bool -> Config

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

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

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

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

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


module Cryptol.Parser.NoInclude
removeIncludes :: Program -> IO (Either [IncludeError] Program)
removeIncludesModule :: Module -> IO (Either [IncludeError] Module)
data IncludeError
IncludeFailed :: (Located FilePath) -> IncludeError
IncludeParseError :: ParseError -> IncludeError
IncludeCycle :: [Located FilePath] -> IncludeError
ppIncludeError :: IncludeError -> Doc
instance GHC.Show.Show Cryptol.Parser.NoInclude.IncludeError
instance GHC.Base.Functor Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Applicative Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Monad Cryptol.Parser.NoInclude.NoIncM


module Cryptol.ModuleSystem.Renamer
data NamingEnv

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

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

-- | Throw errors for any names that overlap in a rewrite environment.
checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning])
class Rename a
rename :: Rename a => a -> RenameM a
runRenamer :: NamingEnv -> RenameM a -> (Either [RenamerError] a, [RenamerWarning])
data RenamerError

-- | Multiple imported symbols contain this name
MultipleSyms :: (Located QName) -> [NameOrigin] -> RenamerError

-- | Expression name is not bound to any definition
UnboundExpr :: (Located QName) -> RenamerError

-- | Type name is not bound to any definition
UnboundType :: (Located QName) -> RenamerError

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

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

-- | When a type is missing from the naming environment, but one or more
--   values exist with the same name.
ExpectedType :: (Located QName) -> RenamerError
data RenamerWarning
SymbolShadowed :: NameOrigin -> [NameOrigin] -> RenamerWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.Out
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Base.Monoid Cryptol.ModuleSystem.Renamer.Out
instance GHC.Base.Functor Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Applicative Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Monad Cryptol.ModuleSystem.Renamer.RenameM
instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename [a]
instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (GHC.Base.Maybe a)
instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.Position.Located a)
instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.AST.Named a)
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Module
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TopDecl
instance Cryptol.ModuleSystem.Renamer.Rename a => Cryptol.ModuleSystem.Renamer.Rename (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Decl
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Newtype
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Schema
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Prop
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Type
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pragma
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Bind
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pattern
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Expr
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TypeInst
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Match
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TySyn


-- | This module contains types used during type inference.
module Cryptol.TypeCheck.InferTypes

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

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

-- | Part of current SCC
CurSCC :: Expr -> Type -> VarType
newtype Goals
Goals :: (TypeMap Goal) -> Goals
emptyGoals :: Goals
nullGoals :: Goals -> Bool
fromGoals :: Goals -> [Goal]
insertGoal :: Goal -> Goals -> Goals

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

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

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

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

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

-- | Signature that gave rise to this constraint
[dctSource] :: DelayedCt -> LQName
[dctForall] :: DelayedCt -> [TParam]
[dctAsmps] :: DelayedCt -> [Prop]
[dctGoals] :: DelayedCt -> [Goal]
data Solved

-- | Solved, assumeing the sub-goals.
Solved :: (Maybe Subst) -> [Goal] -> Solved

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

-- | The goal can never be solved
Unsolvable :: Solved
data Warning
DefaultingKind :: TParam -> Kind -> Warning
DefaultingWildType :: Kind -> Warning
DefaultingTo :: Doc -> Type -> Warning

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

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

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

-- | Number of extra parameters, kind of resut (which should not be of the
--   form <tt>_ -&gt; _</tt>)
TooManyTypeParams :: Int -> Kind -> Error

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

-- | Type-synonym, number of missing params
TooFewTySynParams :: QName -> Int -> Error

-- | Type parameters with the same name (in definition)
RepeatedTyParams :: [TParam] -> Error

-- | Multiple definitions for the same name
RepeatedDefinitions :: QName -> [Range] -> Error

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

-- | Use of a type synonym that was not defined
UndefinedTypeSynonym :: QName -> Error

-- | Use of a variable that was not defined
UndefinedVariable :: QName -> Error

-- | Attempt to explicitly instantiate a non-existent param.
UndefinedTypeParam :: QName -> Error

-- | Multiple definitions for the same type parameter
MultipleTypeParamDefs :: QName -> [Range] -> Error

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

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

-- | A constraint that we could not solve
UnsolvedGoal :: Goal -> Error

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

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

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

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

-- | The given constraint causes the signature of the function to be
--   not-satisfiable.
UnusableFunction :: QName -> Prop -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
AmbiguousType :: [QName] -> Error

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

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

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

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

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

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

-- | Use of a partial type function.
CtPartialTypeFun :: TyFunName -> ConstraintSource
data TyFunName
UserTyFun :: QName -> TyFunName
BuiltInTyFun :: TFun -> TyFunName

-- | For use in error messages
cppKind :: Kind -> Doc
addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc
ppUse :: Expr -> Doc
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goals
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.HasGoal
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Error
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Solved
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.ConstraintSource
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.TyFunName
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Warning
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.TyFunName
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.ConstraintSource
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Warning
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Warning
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Error
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Error
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Subst.FVS Cryptol.TypeCheck.InferTypes.DelayedCt
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goals
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.HasGoal
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.DelayedCt
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Warning
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Error
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Warning)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Error)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.ConstraintSource
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.Goal)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.InferTypes.DelayedCt)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.InferTypes.Solved


module Cryptol.TypeCheck.Monad

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map QName Schema -> Map QName TySyn -> Map QName Newtype -> NameSeeds -> Bool -> InferInput

-- | Location of program source
[inpRange] :: InferInput -> Range

-- | Variables that are in scope
[inpVars] :: InferInput -> Map QName Schema

-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map QName TySyn

-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map QName Newtype

-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds

-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool

-- | This is used for generating various names.
data NameSeeds
NameSeeds :: !Int -> !Int -> NameSeeds
[seedTVar] :: NameSeeds -> !Int
[seedGoal] :: NameSeeds -> !Int

-- | The initial seeds, used when checking a fresh program.
nameSeeds :: NameSeeds

-- | The results of type inference.
data InferOutput a

-- | We found some errors
InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a

-- | Type inference was successful.
InferOK :: [(Range, Warning)] -> NameSeeds -> a -> InferOutput a
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
newtype InferM a
IM :: ReaderT RO (StateT RW IO) a -> InferM a
[unIM] :: InferM a -> ReaderT RO (StateT RW IO) a
data DefLoc
IsLocal :: DefLoc
IsExternal :: DefLoc

-- | Read-only component of the monad.
data RO
RO :: Range -> Map QName VarType -> [TParam] -> Map QName (DefLoc, TySyn) -> Map QName (DefLoc, Newtype) -> Map Int (Expr -> Expr) -> Bool -> RO

-- | Source code being analysed
[iRange] :: RO -> Range

-- | Type of variable that are in scope
[iVars] :: RO -> Map QName VarType

-- | Type variable that are in scope
[iTVars] :: RO -> [TParam]

-- | Type synonyms that are in scope
[iTSyns] :: RO -> Map QName (DefLoc, TySyn)

-- | Newtype declarations in scope
--   
--   NOTE: type synonyms take precedence over newtype. The reason is that
--   we can define local type synonyms, but not local newtypes. So, either
--   a type-synonym shadows a newtype, or it was declared at the top-level,
--   but then there can't be a newtype with the same name (this should be
--   caught by the renamer).
[iNewtypes] :: RO -> Map QName (DefLoc, Newtype)

-- | NOTE: This field is lazy in an important way! It is the final version
--   of <a>iSolvedHas</a> in <a>RW</a>, and the two are tied together
--   through recursion. The field is here so that we can look thing up
--   before they are defined, which is OK because we don't need to know the
--   results until everything is done.
[iSolvedHasLazy] :: RO -> Map Int (Expr -> Expr)

-- | When this flag is set to true, bindings that lack signatures in
--   where-blocks will never be generalized. Bindings with type signatures,
--   and all bindings at top level are unaffected.
[iMonoBinds] :: RO -> Bool

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

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

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

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

-- | These keeps track of what existential type variables are available.
--   When we start checking a function, we push a new scope for its
--   arguments, and we pop it when we are done checking the function body.
--   The front element of the list is the current scope, which is the only
--   thing that will be modified, as follows. When we encounter a
--   existential type variable: 1. we look in all scopes to see if it is
--   already defined. 2. if it was not defined, we create a fresh type
--   variable, and we add it to the current scope. 3. it is an error if we
--   encounter an existential variable but we have no current scope.
[iExistTVars] :: RW -> [Map QName Type]

-- | Selector constraints that have been solved (ref. iSolvedSelectorsLazy)
[iSolvedHas] :: RW -> Map Int (Expr -> Expr)
[iNameSeeds] :: RW -> !NameSeeds

-- | Ordinary constraints
[iCts] :: RW -> !Goals

-- | Tuple/record projection constraints. The <a>Int</a> is the "name" of
--   the constraint, used so that we can name it solution properly.
[iHasCts] :: RW -> ![HasGoal]
io :: IO a -> InferM a

-- | The monadic computation is about the given range of source code. This
--   is useful for error reporting.
inRange :: Range -> InferM a -> InferM a
inRangeMb :: Maybe Range -> InferM a -> InferM a

-- | This is the current range that we are working on.
curRange :: InferM Range

-- | Report an error.
recordError :: Error -> InferM ()
recordWarning :: Warning -> InferM ()
newGoal :: ConstraintSource -> Prop -> InferM Goal

-- | Record some constraints that need to be solved. The string explains
--   where the constraints came from.
newGoals :: ConstraintSource -> [Prop] -> InferM ()

-- | The constraints are removed, and returned to the caller. The
--   substitution IS applied to them.
getGoals :: InferM [Goal]

-- | Add a bunch of goals that need solving.
addGoals :: [Goal] -> InferM ()

-- | Collect the goals emitted by the given sub-computation. Does not emit
--   any new goals.
collectGoals :: InferM a -> InferM (a, [Goal])

-- | Record a constraint that when we select from the first type, we should
--   get a value of the second type. The returned function should be used
--   to wrap the expression from which we are selecting (i.e., the record
--   or tuple). Plese note that the resulting expression should not be
--   forced before the constraint is solved.
newHasGoal :: Selector -> Type -> Type -> InferM (Expr -> Expr)

-- | Add a previously generate has constrained
addHasGoal :: HasGoal -> InferM ()

-- | Get the <tt>Has</tt> constraints. Each of this should either be
--   solved, or added back using <a>addHasGoal</a>.
getHasGoals :: InferM [HasGoal]

-- | Specify the solution (`Expr -&gt; Expr`) for the given constraint
--   (<a>Int</a>).
solveHasGoal :: Int -> (Expr -> Expr) -> InferM ()
newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a

-- | Generate a new name for a goal.
newGoalName :: InferM Int

-- | Generate a new free type variable.
newTVar :: Doc -> Kind -> InferM TVar

-- | Generate a new free type variable that depends on these additional
--   type parameters.
newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar

-- | Generate a new free type variable.
newTParam :: Maybe QName -> Kind -> InferM TParam

-- | Generate an unknown type. The doc is a note about what is this type
--   about.
newType :: Doc -> Kind -> InferM Type

-- | Record that the two types should be syntactically equal.
unify :: Type -> Type -> InferM [Prop]

-- | Apply the accumulated substitution to something with free type
--   variables.
applySubst :: TVars t => t -> InferM t

-- | Get the substitution that we have accumulated so far.
getSubst :: InferM Subst

-- | Add to the accumulated substitution.
extendSubst :: Subst -> InferM ()

-- | Variables that are either mentioned in the environment or in a
--   selector constraint.
varsWithAsmps :: InferM (Set TVar)

-- | Lookup the type of a variable.
lookupVar :: QName -> InferM VarType

-- | Lookup a type variable. Return <a>Nothing</a> if there is no such
--   variable in scope, in which case we must be dealing with a type
--   constant.
lookupTVar :: QName -> InferM (Maybe Type)

-- | Lookup the definition of a type synonym.
lookupTSyn :: QName -> InferM (Maybe TySyn)

-- | Lookup the definition of a newtype
lookupNewtype :: QName -> InferM (Maybe Newtype)

-- | Check if we already have a name for this existential type variable
--   and, if so, return the definition. If not, try to create a new
--   definition, if this is allowed. If not, returns nothing.
existVar :: QName -> Kind -> InferM Type

-- | Returns the type synonyms that are currently in scope.
getTSyns :: InferM (Map QName (DefLoc, TySyn))

-- | Returns the newtype declarations that are in scope.
getNewtypes :: InferM (Map QName (DefLoc, Newtype))

-- | Get the set of bound type variables that are in scope.
getTVars :: InferM (Set QName)

-- | Return the keys of the bound variables that are in scope.
getBoundInScope :: InferM (Set TVar)

-- | Retrieve the value of the `mono-binds` option.
getMonoBinds :: InferM Bool

-- | We disallow shadowing between type synonyms and type variables because
--   it is confusing. As a bonus, in the implementation we don't need to
--   worry about where we lookup things (i.e., in the variable or type
--   synonym environment.
checkTShadowing :: String -> QName -> InferM ()

-- | The sub-computation is performed with the given type parameter in
--   scope.
withTParam :: TParam -> InferM a -> InferM a
withTParams :: [TParam] -> InferM a -> InferM a

-- | The sub-computation is performed with the given type-synonym in scope.
withTySyn :: TySyn -> InferM a -> InferM a
withNewtype :: Newtype -> InferM a -> InferM a

-- | The sub-computation is performed with the given variable in scope.
withVarType :: QName -> VarType -> InferM a -> InferM a
withVarTypes :: [(QName, VarType)] -> InferM a -> InferM a
withVar :: QName -> Schema -> InferM a -> InferM a

-- | The sub-computation is performed with the given variables in scope.
withMonoType :: (QName, Located Type) -> InferM a -> InferM a

-- | The sub-computation is performed with the given variables in scope.
withMonoTypes :: Map QName (Located Type) -> InferM a -> InferM a

-- | The sub-computation is performed with the given type synonyms and
--   variables in scope.
withDecls :: ([TySyn], Map QName Schema) -> InferM a -> InferM a

-- | Perform the given computation in a new scope (i.e., the subcomputation
--   may use existential type variables).
inNewScope :: InferM a -> InferM a
newtype KindM a
KM :: ReaderT KRO (StateT KRW InferM) a -> KindM a
[unKM] :: KindM a -> ReaderT KRO (StateT KRW InferM) a
data KRO
KRO :: Map QName Type -> Bool -> KRO

-- | lazy map, with tyvars.
[lazyTVars] :: KRO -> Map QName Type

-- | are type-wild cards allowed?
[allowWild] :: KRO -> Bool
data KRW
KRW :: Map QName Kind -> KRW

-- | kinds of (known) vars.
[typeParams] :: KRW -> Map QName Kind

-- | The arguments to this function are as follows:
--   
--   (type param. name, kind signature (opt.), a type representing the
--   param)
--   
--   The type representing the parameter is just a thunk that we should not
--   force. The reason is that the type depnds on the kind of parameter,
--   that we are in the process of computing.
--   
--   As a result we return the value of the sub-computation and the
--   computed kinds of the type parameters.
runKindM :: Bool -> [(QName, Maybe Kind, Type)] -> KindM a -> InferM (a, Map QName Kind)

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

-- | Locally bound variable.
TLocalVar :: Type -> (Maybe Kind) -> LkpTyVar

-- | An outer binding.
TOuterVar :: Type -> LkpTyVar

-- | Check if a name refers to a type variable.
kLookupTyVar :: QName -> KindM (Maybe LkpTyVar)

-- | Are type wild-cards OK in this context?
kWildOK :: KindM Bool

-- | Reports an error.
kRecordError :: Error -> KindM ()
kRecordWarning :: Warning -> KindM ()

-- | Generate a fresh unification variable of the given kind.
kNewType :: Doc -> Kind -> KindM Type

-- | Lookup the definition of a type synonym.
kLookupTSyn :: QName -> KindM (Maybe TySyn)

-- | Lookup the definition of a newtype.
kLookupNewtype :: QName -> KindM (Maybe Newtype)
kExistTVar :: QName -> Kind -> KindM Type

-- | Replace the given bound variables with concrete types.
kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type

-- | Record the kind for a local type variable. This assumes that we
--   already checked that there was no other valid kind for the variable
--   (if there was one, it gets over-written).
kSetKind :: QName -> Kind -> KindM ()

-- | The sub-computation is about the given range of the source code.
kInRange :: Range -> KindM a -> KindM a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kInInferM :: InferM a -> KindM a
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.Monad.InferOutput a)
instance GHC.Show.Show Cryptol.TypeCheck.Monad.InferInput
instance GHC.Show.Show Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Base.Functor Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Monad Cryptol.TypeCheck.Monad.InferM
instance Control.Monad.Fix.MonadFix Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Functor Cryptol.TypeCheck.Monad.KindM
instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.KindM
instance GHC.Base.Monad Cryptol.TypeCheck.Monad.KindM


module Cryptol.TypeCheck.Depends
data TyDecl
TS :: TySyn -> TyDecl
NT :: Newtype -> TyDecl

-- | Check for duplicate and recursive type synonyms. Returns the
--   type-synonyms in dependecy order.
orderTyDecls :: [TyDecl] -> InferM [TyDecl]

-- | Associate type signatures with bindings and order bindings by
--   dependency.
orderBinds :: [Bind] -> [SCC Bind]
class FromDecl d
toBind :: FromDecl d => d -> Maybe Bind
toTyDecl :: FromDecl d => d -> Maybe TyDecl
isTopDecl :: FromDecl d => d -> Bool

-- | Given a list of declarations, annoted with (i) the names that they
--   define, and (ii) the names that they use, we compute a list of
--   strongly connected components of the declarations. The SCCs are in
--   dependency order.
mkScc :: [(a, [QName], [QName])] -> [SCC a]

-- | Combine a bunch of definitions into a single map. Here we check that
--   each name is defined only onces.
combineMaps :: [Map QName (Located a)] -> InferM (Map QName (Located a))

-- | Combine a bunch of definitions into a single map. Here we check that
--   each name is defined only onces.
combine :: [(QName, Located a)] -> InferM (Map QName (Located a))

-- | Identify multiple occurances of something.
duplicates :: Ord a => [Located a] -> [(a, [Range])]
instance Cryptol.TypeCheck.Depends.FromDecl Cryptol.Parser.AST.TopDecl
instance Cryptol.TypeCheck.Depends.FromDecl Cryptol.Parser.AST.Decl


module Cryptol.TypeCheck.Instantiate
instantiateWith :: Expr -> Schema -> [Located (Maybe QName, Type)] -> InferM (Expr, Type)


-- | This module contains machinery to reason about ordering of variables,
--   their finiteness, and their possible intervals.
module Cryptol.TypeCheck.Solver.FinOrd
data OrdFacts

-- | Possible outcomes, when asserting a fact.
data AssertResult

-- | We added a new fact
OrdAdded :: OrdFacts -> AssertResult

-- | We already knew this
OrdAlreadyKnown :: AssertResult

-- | Only if the two types are equal
OrdImprove :: Type -> Type -> AssertResult

-- | The fact is known to be false
OrdImpossible :: AssertResult

-- | We could not perform opertaion.
OrdCannot :: AssertResult
noFacts :: OrdFacts
addFact :: IsFact t => t -> OrdFacts -> AssertResult

-- | Query if the one type is known to be smaller than, or equal to, the
--   other. Assumes that the type is simple (i.e., no type functions).
isKnownLeq :: OrdFacts -> Type -> Type -> Bool

-- | Compute an interval, that we know definately contains the given type.
--   Assumes that the type is normalized (i.e., no type functions).
knownInterval :: OrdFacts -> Type -> Interval
ordFactsToGoals :: OrdFacts -> [Goal]
ordFactsToProps :: OrdFacts -> [Prop]

-- | Render facts in <tt>dot</tt> notation. The boolean says if we want the
--   arrows to point up.
dumpDot :: Bool -> OrdFacts -> String
dumpDoc :: OrdFacts -> Doc

-- | Add a `(&gt;=)` or <a>fin</a> goal into the model. Assumes that the
--   types are normalized (i.e., no type functions).
class IsFact t
factProp :: IsFact t => t -> Prop
factChangeProp :: IsFact t => t -> Prop -> t
factSource :: IsFact t => t -> EdgeSrc
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.AssertResult
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.OrdFacts
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Edges
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Edge
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.NumType
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.NumType
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.NumType
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.Nat''
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.Nat''
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.Nat''
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.EdgeSrc
instance GHC.Show.Show Cryptol.TypeCheck.Solver.FinOrd.OrdTerms
instance Cryptol.TypeCheck.Solver.FinOrd.IsFact Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Solver.FinOrd.IsFact Cryptol.TypeCheck.AST.Prop
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.FinOrd.Edge
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.FinOrd.Edge


-- | We define the behavior of Cryptol's type-level functions on integers.
module Cryptol.TypeCheck.Solver.Eval

-- | Collect <tt>fin</tt> and simple <a>&lt;=</a> constraints in the ord
--   model Returns <a>Left</a> if we find a goal which is incompatible with
--   the others. Otherwise, we return <a>Right</a> with a model, and the
--   remaining (i.e., the non-order related) properties.
--   
--   These sorts of facts are quite useful during type simplification,
--   because they provide information which potentially useful for
--   cancellation (e.g., this variables is finite and not 0)
assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])

-- | This returns order properties that are implied by the give property.
--   It is important that the returned properties are propoer ordering
--   properties (i.e., <a>addFact</a> will not return <a>OrdCannot</a>).
derivedOrd :: OrdFacts -> Prop -> [Prop]
isSimpleType :: Type -> Bool
simpType :: OrdFacts -> Type -> Type
reorderArgs :: TFun -> [Type] -> [Type]
commuteArgs :: [Type] -> [Type]
evalTFun :: OrdFacts -> TFun -> [Type] -> Maybe Type
typeInterval :: OrdFacts -> Type -> Interval
typeKnownLeq :: OrdFacts -> Type -> Type -> Bool
typeKnownFin :: OrdFacts -> Type -> Bool
tfAdd :: OrdFacts -> Type -> Type -> Maybe Type

-- | <tt>tfSub x y = Just z</tt> iff <tt>z</tt> is the unique value such
--   that <tt>tfAdd y z = Just x</tt>
tfSub :: OrdFacts -> Type -> Type -> Maybe Type

-- | It is important that the 0 rules come before the <a>Inf</a> ones
tfMul :: OrdFacts -> Type -> Type -> Maybe Type
tfDiv :: OrdFacts -> Type -> Type -> Maybe Type
tfMod :: OrdFacts -> Type -> Type -> Maybe Type
tfMin :: OrdFacts -> Type -> Type -> Maybe Type
tfMax :: OrdFacts -> Type -> Type -> Maybe Type
tfExp :: OrdFacts -> Type -> Type -> Maybe Type

-- | Rounds up <tt>lg2 x = Just y</tt>, if <tt>y</tt> is the smallest
--   number such that <tt>x &lt;= 2 ^ y</tt>
tfLg2 :: OrdFacts -> Type -> Maybe Type

-- | XXX: <tt>width</tt> and <tt>lg2</tt> are almost the same! <tt>width n
--   == lg2 (n + 1)</tt>
tfWidth :: OrdFacts -> Type -> Maybe Type
tfLenFromThen :: OrdFacts -> Type -> Type -> Type -> Maybe Type
tfLenFromThenTo :: OrdFacts -> Type -> Type -> Type -> Maybe Type
toNat' :: Type -> Maybe Nat'
fromNat' :: Nat' -> Type
oneOrMore :: OrdFacts -> Type -> Bool
twoOrMore :: OrdFacts -> Type -> Bool


-- | Solver code that does not depend on the type inference monad.
module Cryptol.TypeCheck.Solver.Numeric

-- | Try to perform a single step of simplification for a numeric goal. We
--   assume that the substitution has been applied to the goal.
numericStep :: OrdFacts -> Goal -> Solved
simpFin :: OrdFacts -> Prop -> Maybe [Prop]

-- | Collect <tt>fin</tt> and <a>&lt;=</a> constraints in the ord model
--   Returns (new model, bad goals, other goals). "bad goals" are goals
--   that are incompatible with the model "other goals" are ones that are
--   not "&lt;=" or "fin"
goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal])


module Cryptol.TypeCheck.Defaulting
tryDefault :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
tryDefaultWith :: OrdFacts -> [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])

-- | Try to pick a reasonable instantiation for an expression, with the
--   given type. This is useful when we do evaluation at the REPL. The
--   resaulting types should satisfy the constraints of the schema.
defaultExpr :: Range -> Expr -> Schema -> Maybe ([(TParam, Type)], Expr)


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

-- | Solve class constraints.
classStep :: Goal -> Solved

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


module Cryptol.TypeCheck.Solver.Selector

-- | Solve has-constraints.
tryHasGoal :: HasGoal -> InferM ()


module Cryptol.TypeCheck.Solver.Smtlib
simpDelayed :: [TParam] -> OrdFacts -> [Prop] -> [Goal] -> IO [Goal]
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Smtlib.SMTResult
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Smtlib.SMTResult


module Cryptol.TypeCheck.Solve
simplifyAllConstraints :: InferM ()
proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst

-- | Collect <tt>fin</tt> and simple <a>&lt;=</a> constraints in the ord
--   model Returns <a>Left</a> if we find a goal which is incompatible with
--   the others. Otherwise, we return <a>Right</a> with a model, and the
--   remaining (i.e., the non-order related) properties.
--   
--   These sorts of facts are quite useful during type simplification,
--   because they provide information which potentially useful for
--   cancellation (e.g., this variables is finite and not 0)
assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])
checkTypeFunction :: TFun -> [Type] -> [Prop]


module Cryptol.TypeCheck.Kind
checkType :: Type -> Maybe Kind -> InferM Type

-- | Check a type signature.
checkSchema :: Schema -> InferM (Schema, [Goal])

-- | Check a newtype declaration. XXX: Do something with constraints.
checkNewtype :: Newtype -> InferM Newtype

-- | Check a type-synonym declaration.
checkTySyn :: TySyn -> InferM TySyn


-- | Assumes that the <tt>NoPat</tt> pass has been run.
module Cryptol.TypeCheck.Infer
inferModule :: Module -> InferM Module
desugarLiteral :: Bool -> Literal -> InferM Expr

-- | Infer the type of an expression with an explicit instantiation.
appTys :: Expr -> [Located (Maybe QName, Type)] -> Type -> InferM Expr
inferTyParam :: TypeInst -> InferM (Located (Maybe QName, Type))
checkTypeOfKind :: Type -> Kind -> InferM Type

-- | We use this when we want to ensure that the expr has exactly
--   (syntactically) the given type.
inferE :: Doc -> Expr -> InferM (Expr, Type)

-- | Infer the type of an expression, and translate it to a fully
--   elaborated core term.
checkE :: Expr -> Type -> InferM Expr
expectSeq :: Type -> InferM (Type, Type)
expectTuple :: Int -> Type -> InferM [Type]
expectRec :: [Named a] -> Type -> InferM [(Name, a, Type)]
expectFin :: Int -> Type -> InferM ()
expectFun :: Int -> Type -> InferM ([Type], Type)
checkHasType :: Expr -> Type -> Type -> InferM Expr
checkFun :: Doc -> [Pattern] -> Expr -> Type -> InferM Expr

-- | The type the is the smallest of all
smallest :: [Type] -> InferM Type
checkP :: Doc -> Pattern -> Type -> InferM (Located QName)

-- | Infer the type of a pattern. Assumes that the pattern will be just a
--   variable.
inferP :: Doc -> Pattern -> InferM (QName, Located Type)

-- | Infer the type of one match in a list comprehension.
inferMatch :: Match -> InferM (Match, QName, Located Type, Type)

-- | Infer the type of one arm of a list comprehension.
inferCArm :: Int -> [Match] -> InferM ([Match], Map QName (Located Type), Type)

-- | <tt>inferBinds isTopLevel isRec binds</tt> performs inference for a
--   strongly-connected component of <a>Bind</a>s. If <tt>isTopLevel</tt>
--   is true, any bindings without type signatures will be generalized. If
--   it is false, and the mono-binds flag is enabled, no bindings without
--   type signatures will be generalized, but bindings with signatures will
--   be unaffected.
inferBinds :: Bool -> Bool -> [Bind] -> InferM [Decl]

-- | Come up with a type for recursive calls to a function, and decide how
--   we are going to be checking the binding. Returns: (Name, type or
--   schema, computation to check binding)
--   
--   The <tt>exprMap</tt> is a thunk where we can lookup the final
--   expressions and we should be careful not to force it.
guessType :: Map QName Expr -> Bind -> InferM ((QName, VarType), Either (InferM Decl) (InferM Decl))

-- | Try to evaluate the inferred type of a mono-binding
simpMonoBind :: OrdFacts -> Decl -> Decl

-- | The inputs should be declarations with monomorphic types (i.e., of the
--   form `Forall [] [] t`).
generalize :: [Decl] -> [Goal] -> InferM [Decl]
checkMonoB :: Bind -> Type -> InferM Decl
checkSigB :: Bind -> (Schema, [Goal]) -> InferM Decl
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
tcPanic :: String -> [String] -> a


module Cryptol.TypeCheck
tcModule :: Module -> InferInput -> IO (InferOutput Module)
tcExpr :: Expr -> InferInput -> IO (InferOutput (Expr, Schema))
tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map QName Schema -> Map QName TySyn -> Map QName Newtype -> NameSeeds -> Bool -> InferInput

-- | Location of program source
[inpRange] :: InferInput -> Range

-- | Variables that are in scope
[inpVars] :: InferInput -> Map QName Schema

-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map QName TySyn

-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map QName Newtype

-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds

-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool

-- | The results of type inference.
data InferOutput a

-- | We found some errors
InferFailed :: [(Range, Warning)] -> [(Range, Error)] -> InferOutput a

-- | Type inference was successful.
InferOK :: [(Range, Warning)] -> NameSeeds -> a -> InferOutput a

-- | This is used for generating various names.
data NameSeeds

-- | The initial seeds, used when checking a fresh program.
nameSeeds :: NameSeeds

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

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

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

-- | Number of extra parameters, kind of resut (which should not be of the
--   form <tt>_ -&gt; _</tt>)
TooManyTypeParams :: Int -> Kind -> Error

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

-- | Type-synonym, number of missing params
TooFewTySynParams :: QName -> Int -> Error

-- | Type parameters with the same name (in definition)
RepeatedTyParams :: [TParam] -> Error

-- | Multiple definitions for the same name
RepeatedDefinitions :: QName -> [Range] -> Error

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

-- | Use of a type synonym that was not defined
UndefinedTypeSynonym :: QName -> Error

-- | Use of a variable that was not defined
UndefinedVariable :: QName -> Error

-- | Attempt to explicitly instantiate a non-existent param.
UndefinedTypeParam :: QName -> Error

-- | Multiple definitions for the same type parameter
MultipleTypeParamDefs :: QName -> [Range] -> Error

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

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

-- | A constraint that we could not solve
UnsolvedGoal :: Goal -> Error

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

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

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

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

-- | The given constraint causes the signature of the function to be
--   not-satisfiable.
UnusableFunction :: QName -> Prop -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
AmbiguousType :: [QName] -> Error
data Warning
DefaultingKind :: TParam -> Kind -> Warning
DefaultingWildType :: Kind -> Warning
DefaultingTo :: Doc -> Type -> Warning
ppWarning :: (Range, Warning) -> Doc
ppError :: (Range, Error) -> Doc


module Cryptol.ModuleSystem.Env
data ModuleEnv
ModuleEnv :: LoadedModules -> NameSeeds -> EvalEnv -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Bool -> ModuleEnv
[meLoadedModules] :: ModuleEnv -> LoadedModules
[meNameSeeds] :: ModuleEnv -> NameSeeds
[meEvalEnv] :: ModuleEnv -> EvalEnv
[meFocusedModule] :: ModuleEnv -> Maybe ModName
[meSearchPath] :: ModuleEnv -> [FilePath]
[meDynEnv] :: ModuleEnv -> DynamicEnv
[meMonoBinds] :: ModuleEnv -> !Bool
resetModuleEnv :: ModuleEnv -> ModuleEnv
initialModuleEnv :: IO ModuleEnv

-- | Try to focus a loaded module in the module environment.
focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv

-- | Get a list of all the loaded modules. Each module in the resulting
--   list depends only on other modules that precede it.
loadedModules :: ModuleEnv -> [Module]

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system.
--   
--   This could really do with some better error handling, just returning
--   mempty when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> IfaceDecls

-- | Produce an ifaceDecls that represents the internal environment of the
--   module, used for typechecking.
qualifiedEnv :: ModuleEnv -> IfaceDecls
loadModuleEnv :: (Import -> Iface -> Iface) -> ModuleEnv -> Maybe (Iface, IfaceDecls)

-- | Invariant: All the dependencies of any module <tt>m</tt> must precede
--   <tt>m</tt> in the list.
newtype LoadedModules
LoadedModules :: [LoadedModule] -> LoadedModules
[getLoadedModules] :: LoadedModules -> [LoadedModule]
data LoadedModule
LoadedModule :: ModName -> FilePath -> Iface -> Module -> LoadedModule
[lmName] :: LoadedModule -> ModName
[lmFilePath] :: LoadedModule -> FilePath
[lmInterface] :: LoadedModule -> Iface
[lmModule] :: LoadedModule -> Module
isLoaded :: ModName -> LoadedModules -> Bool
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
addLoadedModule :: FilePath -> Module -> LoadedModules -> LoadedModules
removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules

-- | Extra information we need to carry around to dynamically extend an
--   environment outside the context of a single module. Particularly
--   useful when dealing with interactive declarations as in <tt>:let</tt>
--   or <tt>it</tt>.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv

-- | Build <a>IfaceDecls</a> that correspond to all of the bindings in the
--   dynamic environment.
--   
--   XXX: if we ever add type synonyms or newtypes at the REPL, revisit
--   this.
deIfaceDecls :: DynamicEnv -> IfaceDecls
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModule
instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Base.Monoid Cryptol.ModuleSystem.Env.DynamicEnv


module Cryptol.ModuleSystem.Monad
data ImportSource
FromModule :: ModName -> ImportSource
FromImport :: (Located Import) -> ImportSource
importedModule :: ImportSource -> ModName
data ModuleError

-- | Unable to find the module given, tried looking in these paths
ModuleNotFound :: ModName -> [FilePath] -> ModuleError

-- | Unable to open a file
CantFindFile :: FilePath -> ModuleError

-- | Some other IO error occurred while reading this file
OtherIOError :: FilePath -> IOException -> ModuleError

-- | Generated this parse error when parsing the file for module m
ModuleParseError :: FilePath -> ParseError -> ModuleError

-- | Recursive module group discovered
RecursiveModules :: [ImportSource] -> ModuleError

-- | Problems during the renaming phase
RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError

-- | Problems during the NoPat phase
NoPatErrors :: ImportSource -> [Error] -> ModuleError

-- | Problems during the NoInclude phase
NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError

-- | Problems during type checking
TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError

-- | Problems after type checking, eg. specialization
OtherFailure :: String -> ModuleError

-- | Module loaded by 'import' statement has the wrong module name
ModuleNameMismatch :: ModName -> (Located ModName) -> ModuleError

-- | Two modules loaded from different files have the same module name
DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError
moduleNotFound :: ModName -> [FilePath] -> ModuleM a
cantFindFile :: FilePath -> ModuleM a
otherIOError :: FilePath -> IOException -> ModuleM a
moduleParseError :: FilePath -> ParseError -> ModuleM a
recursiveModules :: [ImportSource] -> ModuleM a
renamerErrors :: [RenamerError] -> ModuleM a
noPatErrors :: [Error] -> ModuleM a
noIncludeErrors :: [IncludeError] -> ModuleM a
typeCheckingFailed :: [(Range, Error)] -> ModuleM a
moduleNameMismatch :: ModName -> Located ModName -> ModuleM a
duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a
data ModuleWarning
TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning
RenamerWarnings :: [RenamerWarning] -> ModuleWarning
warn :: [ModuleWarning] -> ModuleM ()
typeCheckWarnings :: [(Range, Warning)] -> ModuleM ()
renamerWarnings :: [RenamerWarning] -> ModuleM ()
data RO
RO :: [ImportSource] -> RO
[roLoading] :: RO -> [ImportSource]
emptyRO :: RO
newtype ModuleT m a
ModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a -> ModuleT m a
[unModuleT] :: ModuleT m a -> ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
runModuleT :: Monad m => ModuleEnv -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
type ModuleM = ModuleT IO
runModuleM :: ModuleEnv -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
io :: BaseM m IO => IO a -> ModuleT m a
getModuleEnv :: Monad m => ModuleT m ModuleEnv
setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m ()
isLoaded :: ModName -> ModuleM Bool
loadingImport :: Located Import -> ModuleM a -> ModuleM a
loadingModule :: ModName -> ModuleM a -> ModuleM a

-- | Push an "interactive" context onto the loading stack. A bit of a hack,
--   as it uses a faked module name
interactive :: ModuleM a -> ModuleM a
loading :: ImportSource -> ModuleM a -> ModuleM a

-- | Get the currently focused import source.
getImportSource :: ModuleM ImportSource
getIface :: ModName -> ModuleM Iface
getNameSeeds :: ModuleM NameSeeds
getMonoBinds :: ModuleM Bool
setMonoBinds :: Bool -> ModuleM ()
setNameSeeds :: NameSeeds -> ModuleM ()

-- | Remove a module from the set of loaded module, by its path.
unloadModule :: FilePath -> ModuleM ()
loadedModule :: FilePath -> Module -> ModuleM ()
modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM ()
getEvalEnv :: ModuleM EvalEnv
getFocusedModule :: ModuleM (Maybe ModName)
setFocusedModule :: ModName -> ModuleM ()
getSearchPath :: ModuleM [FilePath]

-- | Run a <a>ModuleM</a> action in a context with a prepended search path.
--   Useful for temporarily looking in other places while resolving
--   imports, for example.
withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
getFocusedEnv :: ModuleM IfaceDecls
getQualifiedEnv :: ModuleM IfaceDecls
getDynEnv :: ModuleM DynamicEnv
setDynEnv :: DynamicEnv -> ModuleM ()
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleError
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Classes.Eq Cryptol.ModuleSystem.Monad.ImportSource
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ImportSource
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Base.Monad m => GHC.Base.Functor (Cryptol.ModuleSystem.Monad.ModuleT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Cryptol.ModuleSystem.Monad.ModuleT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Cryptol.ModuleSystem.Monad.ModuleT m)
instance MonadLib.MonadT Cryptol.ModuleSystem.Monad.ModuleT


module Cryptol.ModuleSystem.Base
rename :: Rename a => NamingEnv -> a -> ModuleM a

-- | Rename a module in the context of its imported modules.
renameModule :: Module -> ModuleM Module

-- | Rename an expression in the context of the focused module.
renameExpr :: Expr -> ModuleM Expr

-- | Rename declarations in the context of the focused module.
renameDecls :: (Rename d, FromDecl d) => [d] -> ModuleM [d]

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
parseModule :: FilePath -> ModuleM Module

-- | Load a module by its path.
loadModuleByPath :: FilePath -> ModuleM Module

-- | Load the module specified by an import.
loadImport :: Located Import -> ModuleM ()

-- | Load dependencies, typecheck, and add to the eval environment.
loadModule :: FilePath -> Module -> ModuleM Module

-- | Rewrite an import declaration to be of the form:
--   
--   <pre>
--   import foo as foo [ [hiding] (a,b,c) ]
--   </pre>
fullyQualified :: Import -> Import

-- | Process the interface specified by an import.
importIface :: Import -> ModuleM Iface

-- | Load a series of interfaces, merging their public interfaces.
importIfaces :: [Import] -> ModuleM IfaceDecls
moduleFile :: ModName -> String -> FilePath

-- | Discover a module.
findModule :: ModName -> ModuleM FilePath

-- | Discover a file. This is distinct from <a>findModule</a> in that we
--   assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath
preludeName :: ModName

-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: Module -> Module

-- | Load the dependencies of a module into the environment.
loadDeps :: Module -> ModuleM ()

-- | Typecheck a single expression.
checkExpr :: Expr -> ModuleM (Expr, Schema)

-- | Typecheck a group of declarations.
checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleM [DeclGroup]

-- | Typecheck a module.
checkModule :: Module -> ModuleM Module
type TCAction i o = i -> InferInput -> IO (InferOutput o)
typecheck :: HasLoc i => TCAction i o -> i -> IfaceDecls -> ModuleM o

-- | Process a list of imports, producing an aggregate interface suitable
--   for use when typechecking.
importIfacesTc :: [Import] -> ModuleM IfaceDecls

-- | Generate input for the typechecker.
genInferInput :: Range -> IfaceDecls -> ModuleM InferInput
evalExpr :: Expr -> ModuleM Value
evalDecls :: [DeclGroup] -> ModuleM ()


module Cryptol.ModuleSystem
data ModuleEnv
ModuleEnv :: LoadedModules -> NameSeeds -> EvalEnv -> Maybe ModName -> [FilePath] -> DynamicEnv -> !Bool -> ModuleEnv
[meLoadedModules] :: ModuleEnv -> LoadedModules
[meNameSeeds] :: ModuleEnv -> NameSeeds
[meEvalEnv] :: ModuleEnv -> EvalEnv
[meFocusedModule] :: ModuleEnv -> Maybe ModName
[meSearchPath] :: ModuleEnv -> [FilePath]
[meDynEnv] :: ModuleEnv -> DynamicEnv
[meMonoBinds] :: ModuleEnv -> !Bool
initialModuleEnv :: IO ModuleEnv

-- | Extra information we need to carry around to dynamically extend an
--   environment outside the context of a single module. Particularly
--   useful when dealing with interactive declarations as in <tt>:let</tt>
--   or <tt>it</tt>.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv
data ModuleError

-- | Unable to find the module given, tried looking in these paths
ModuleNotFound :: ModName -> [FilePath] -> ModuleError

-- | Unable to open a file
CantFindFile :: FilePath -> ModuleError

-- | Some other IO error occurred while reading this file
OtherIOError :: FilePath -> IOException -> ModuleError

-- | Generated this parse error when parsing the file for module m
ModuleParseError :: FilePath -> ParseError -> ModuleError

-- | Recursive module group discovered
RecursiveModules :: [ImportSource] -> ModuleError

-- | Problems during the renaming phase
RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError

-- | Problems during the NoPat phase
NoPatErrors :: ImportSource -> [Error] -> ModuleError

-- | Problems during the NoInclude phase
NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError

-- | Problems during type checking
TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError

-- | Problems after type checking, eg. specialization
OtherFailure :: String -> ModuleError

-- | Module loaded by 'import' statement has the wrong module name
ModuleNameMismatch :: ModName -> (Located ModName) -> ModuleError

-- | Two modules loaded from different files have the same module name
DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError
data ModuleWarning
TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning
RenamerWarnings :: [RenamerWarning] -> ModuleWarning
type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])

-- | Find the file associated with a module name in the module search path.
findModule :: ModName -> ModuleCmd FilePath

-- | Load the module contained in the given file.
loadModuleByPath :: FilePath -> ModuleCmd Module

-- | Load the given parsed module.
loadModule :: FilePath -> Module -> ModuleCmd Module

-- | Check the type of an expression.
checkExpr :: Expr -> ModuleCmd (Expr, Schema)

-- | Evaluate an expression.
evalExpr :: Expr -> ModuleCmd Value

-- | Typecheck declarations.
checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleCmd [DeclGroup]

-- | Evaluate declarations and add them to the extended environment.
evalDecls :: [DeclGroup] -> ModuleCmd ()
noPat :: RemovePatterns a => a -> ModuleCmd a

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system.
--   
--   This could really do with some better error handling, just returning
--   mempty when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> IfaceDecls

-- | The resulting interface generated by a module that has been
--   typechecked.
data Iface
Iface :: ModName -> IfaceDecls -> IfaceDecls -> Iface
[ifModName] :: Iface -> ModName
[ifPublic] :: Iface -> IfaceDecls
[ifPrivate] :: Iface -> IfaceDecls
data IfaceDecls
IfaceDecls :: Map QName [IfaceTySyn] -> Map QName [IfaceNewtype] -> Map QName [IfaceDecl] -> IfaceDecls
[ifTySyns] :: IfaceDecls -> Map QName [IfaceTySyn]
[ifNewtypes] :: IfaceDecls -> Map QName [IfaceNewtype]
[ifDecls] :: IfaceDecls -> Map QName [IfaceDecl]

-- | Generate an Iface from a typechecked module.
genIface :: Module -> Iface
type IfaceTySyn = TySyn
data IfaceDecl
IfaceDecl :: QName -> Schema -> [Pragma] -> IfaceDecl
[ifDeclName] :: IfaceDecl -> QName
[ifDeclSig] :: IfaceDecl -> Schema
[ifDeclPragmas] :: IfaceDecl -> [Pragma]


module Cryptol.Transform.Specialize

-- | A QName should have an entry in the SpecCache iff it is specializable.
--   Each QName starts out with an empty TypesMap.
type SpecCache = Map QName (Decl, TypesMap (QName, Maybe Decl))

-- | The specializer monad.
type SpecT m a = StateT SpecCache (ModuleT m) a
type SpecM a = SpecT IO a
runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
liftSpecT :: Monad m => ModuleT m a -> SpecT m a
getSpecCache :: Monad m => SpecT m SpecCache
setSpecCache :: Monad m => SpecCache -> SpecT m ()
modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m ()
modify :: StateM m s => (s -> s) -> m ()

-- | Add a `where` clause to the given expression containing
--   type-specialized versions of all functions called (transitively) by
--   the body of the expression.
specialize :: Expr -> ModuleCmd Expr
specializeExpr :: Expr -> SpecM Expr
specializeMatch :: Match -> SpecM Match

-- | Add the declarations to the SpecCache, run the given monadic action,
--   and then pull the specialized declarations back out of the SpecCache
--   state. Return the result along with the declarations and a table of
--   names of specialized bindings.
withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map QName (TypesMap QName))

-- | Compute the specialization of `EWhere e dgs`. A decl within
--   <tt>dgs</tt> is replicated once for each monomorphic type instance at
--   which it is used; decls not mentioned in <tt>e</tt> (even monomorphic
--   ones) are simply dropped.
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr

-- | Transform the given declaration groups into a set of monomorphic
--   declarations. All of the original declarations with monomorphic types
--   are kept; additionally the result set includes instantiated versions
--   of polymorphic decls that are referenced by the monomorphic bindings.
--   We also return a map relating generated names to the names from the
--   original declarations.
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map QName (TypesMap QName))
specializeConst :: Expr -> SpecM Expr
destEProofApps :: Expr -> (Expr, Int)
destETApps :: Expr -> (Expr, [Type])
destEProofAbs :: Expr -> ([Prop], Expr)
destETAbs :: Expr -> ([TParam], Expr)
freshName :: QName -> [Type] -> SpecM QName
matchingBoundNames :: (Maybe ModName) -> SpecM [String]
reifyName :: Name -> [Type] -> String
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema

-- | Reduce `length ts` outermost type abstractions and <tt>n</tt> proof
--   abstractions.
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
allDeclGroups :: ModuleEnv -> [DeclGroup]
allLoadedModules :: ModuleEnv -> [LoadedModule]
allPublicQNames :: ModuleEnv -> [QName]
traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)


module Cryptol.Symbolic.Prims
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
evalECon :: ECon -> Value
selectV :: (Integer -> Value) -> Value -> Value
replicateV :: Integer -> TValue -> Value -> Value
nth :: a -> [a] -> Int -> a
nthV :: Value -> Value -> Integer -> Value
mapV :: Bool -> (Value -> Value) -> Value -> Value
catV :: Value -> Value -> Value
dropV :: Integer -> Value -> Value
takeV :: Integer -> Value -> Value

-- | Make a numeric constant. { val, bits } (fin val, fin bits, bits &gt;=
--   width val) =&gt; [bits]
ecDemoteV :: Value

-- | An easy-to-use alternative representation for type <a>TValue</a>.
data TypeVal
TVBit :: TypeVal
TVSeq :: Int -> TypeVal -> TypeVal
TVStream :: TypeVal -> TypeVal
TVTuple :: [TypeVal] -> TypeVal
TVRecord :: [(Name, TypeVal)] -> TypeVal
TVFun :: TypeVal -> TypeVal -> TypeVal
toTypeVal :: TValue -> TypeVal
type Binary = TValue -> Value -> Value -> Value
type Unary = TValue -> Value -> Value

-- | Models functions of type `{a} (Arith a) =&gt; a -&gt; a -&gt; a`
arithBinary :: (SWord -> SWord -> SWord) -> Binary

-- | Models functions of type `{a} (Arith a) =&gt; a -&gt; a`
arithUnary :: (SWord -> SWord) -> Unary
sExp :: SWord -> SWord -> SWord

-- | Ceiling (log_2 x)
sLg2 :: SWord -> SWord
cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> (Value -> Value -> a -> a)
cmpEq :: SWord -> SWord -> SBool -> SBool
cmpNotEq :: SWord -> SWord -> SBool -> SBool
cmpLt :: SWord -> SWord -> SBool -> SBool
cmpGt :: SWord -> SWord -> SBool -> SBool
cmpLtEq :: SWord -> SWord -> SBool -> SBool
cmpGtEq :: SWord -> SWord -> SBool -> SBool
cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary
errorV :: String -> TValue -> Value
zeroV :: TValue -> Value

-- | Join a sequence of sequences into a single sequence.
joinV :: TValue -> TValue -> TValue -> Value -> Value

-- | Split implementation.
ecSplitV :: Value

-- | Split into infinitely many chunks
infChunksOf :: Integer -> [a] -> [[a]]

-- | Split into finitely many chunks
finChunksOf :: Integer -> Integer -> [a] -> [[a]]

-- | Merge two values given a binop. This is used for and, or and xor.
logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary
logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary
fromThenV :: Value
fromToV :: Value
fromThenToV :: Value

-- | Add two polynomials
addPoly :: [SBool] -> [SBool] -> [SBool]
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
degree :: [SBool] -> Int
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
idx :: [SBool] -> Int -> SBool
divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])


module Cryptol.Symbolic
smtMode :: SMTLibVersion
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 -> [DeclGroup] -> Maybe FilePath -> Expr -> Schema -> ProverCommand

-- | The type of query to run
[pcQueryType] :: ProverCommand -> QueryType

-- | Which prover to use (one of the strings in <a>proverConfigs</a>)
[pcProverName] :: ProverCommand -> String

-- | Verbosity flag passed to SBV
[pcVerbose] :: ProverCommand -> Bool

-- | 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 <a>Schema</a> of <tt>pcExpr</tt>
[pcSchema] :: ProverCommand -> Schema

-- | 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 ProverResult
satProve :: ProverCommand -> ModuleCmd ProverResult
satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
parseValues :: [FinType] -> [CW] -> ([Value], [CW])
parseValue :: FinType -> [CW] -> (Value, [CW])
allDeclGroups :: ModuleEnv -> [DeclGroup]
data FinType
FTBit :: FinType
FTSeq :: Int -> FinType -> FinType
FTTuple :: [FinType] -> FinType
FTRecord :: [(Name, FinType)] -> FinType
numType :: Type -> Maybe Int
finType :: Type -> Maybe FinType
unFinType :: FinType -> Type
predArgTypes :: Schema -> Either String [FinType]
forallFinType :: FinType -> Symbolic Value
existsFinType :: FinType -> Symbolic Value
data Env
Env :: Map QName Value -> Map TVar TValue -> Env
[envVars] :: Env -> Map QName Value
[envTypes] :: Env -> Map TVar TValue
emptyEnv :: Env

-- | Bind a variable in the evaluation environment.
bindVar :: (QName, Value) -> Env -> Env

-- | Lookup a variable in the environment.
lookupVar :: QName -> Env -> Maybe Value

-- | Bind a type variable of kind *.
bindType :: TVar -> TValue -> Env -> Env

-- | Lookup a type variable.
lookupType :: TVar -> Env -> Maybe TValue
evalExpr :: Env -> Expr -> Value
evalType :: Env -> Type -> TValue
evalSel :: Selector -> Value -> Value
evalDecls :: Env -> [DeclGroup] -> Env
evalDeclGroup :: Env -> DeclGroup -> Env
evalDecl :: Env -> Decl -> (QName, Value)

-- | Make a copy of the given value, building the spine based only on the
--   type without forcing the value argument. This lets us avoid strictness
--   problems when evaluating recursive definitions.
copyBySchema :: Env -> Schema -> Value -> Value
copyByType :: Env -> TValue -> Value -> Value

-- | Evaluate a comprehension.
evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value

-- | Turn a list of matches into the final environments for each iteration
--   of the branch.
branchEnvs :: Env -> [Match] -> [Env]

-- | Turn a match into the list of environments it represents.
evalMatch :: Env -> Match -> [Env]
instance GHC.Show.Show Cryptol.Symbolic.QueryType
instance GHC.Show.Show Cryptol.Symbolic.SatNum
instance GHC.Base.Monoid Cryptol.Symbolic.Env


module Cryptol.REPL.Monad

-- | REPL_ context with InputT handling.
newtype REPL a
REPL :: (IORef RW -> IO a) -> REPL a
[unREPL] :: REPL a -> IORef RW -> IO a

-- | Run a REPL action with a fresh environment.
runREPL :: Bool -> REPL a -> IO a
io :: IO a -> REPL a

-- | Raise an exception.
raise :: REPLException -> REPL a
stop :: REPL ()
catch :: REPL a -> (REPLException -> REPL a) -> REPL a

-- | Use the configured output action to print a string with a trailing
--   newline
rPutStrLn :: String -> REPL ()

-- | Use the configured output action to print a string
rPutStr :: String -> REPL ()

-- | Use the configured output action to print something using its Show
--   instance
rPrint :: Show a => a -> REPL ()

-- | REPL exceptions.
data REPLException
ParseError :: ParseError -> REPLException
FileNotFound :: FilePath -> REPLException
DirectoryNotFound :: FilePath -> REPLException
NoPatError :: [Error] -> REPLException
NoIncludeError :: [IncludeError] -> REPLException
EvalError :: EvalError -> REPLException
ModuleSystemError :: ModuleError -> REPLException
EvalPolyError :: Schema -> REPLException
TypeNotTestable :: Type -> REPLException
rethrowEvalError :: IO a -> IO a
getModuleEnv :: REPL ModuleEnv
setModuleEnv :: ModuleEnv -> REPL ()
getDynEnv :: REPL DynamicEnv
setDynEnv :: DynamicEnv -> REPL ()

-- | Given an existing qualified name, prefix it with a relatively-unique
--   string. We make it unique by prefixing with a character <tt>#</tt>
--   that is not lexically valid in a module name.
uniqify :: QName -> REPL QName
getTSyns :: REPL (Map QName TySyn)
getNewtypes :: REPL (Map QName Newtype)
getVars :: REPL (Map QName IfaceDecl)
whenDebug :: REPL () -> REPL ()

-- | Get visible variable names.
getExprNames :: REPL [String]

-- | Get visible type signature names.
getTypeNames :: REPL [String]
getPropertyNames :: REPL [String]
data LoadedModule
LoadedModule :: Maybe ModName -> FilePath -> LoadedModule

-- | Focused module
[lName] :: LoadedModule -> Maybe ModName

-- | Focused file
[lPath] :: LoadedModule -> FilePath
getLoadedMod :: REPL (Maybe LoadedModule)

-- | Set the name of the currently focused file, edited by <tt>:e</tt> and
--   loaded via <tt>:r</tt>.
setLoadedMod :: LoadedModule -> REPL ()
setSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [FilePath] -> REPL ()
builtIns :: [(String, (ECon, Schema))]

-- | Construct the prompt for the current environment.
getPrompt :: REPL String
shouldContinue :: REPL Bool
unlessBatch :: REPL () -> REPL ()

-- | Run a computation in batch mode, restoring the previous isBatch flag
--   afterwards
asBatch :: REPL () -> REPL ()
disableLet :: REPL ()
enableLet :: REPL ()

-- | Are let-bindings enabled in this REPL?
getLetEnabled :: REPL Bool

-- | Update the title
updateREPLTitle :: REPL ()

-- | Set the function that will be called when updating the title
setUpdateREPLTitle :: REPL () -> REPL ()
data EnvVal
EnvString :: String -> EnvVal
EnvNum :: !Int -> EnvVal
EnvBool :: Bool -> EnvVal
data OptionDescr
OptionDescr :: String -> EnvVal -> (EnvVal -> IO (Maybe String)) -> String -> (EnvVal -> REPL ()) -> OptionDescr
[optName] :: OptionDescr -> String
[optDefault] :: OptionDescr -> EnvVal
[optCheck] :: OptionDescr -> EnvVal -> IO (Maybe String)
[optHelp] :: OptionDescr -> String
[optEff] :: OptionDescr -> EnvVal -> REPL ()

-- | Set a user option.
setUser :: String -> String -> REPL ()

-- | Get a user option, when it's known to exist. Fail with panic when it
--   doesn't.
getUser :: String -> REPL EnvVal

-- | Get a user option, using Maybe for failure.
tryGetUser :: String -> REPL (Maybe EnvVal)
userOptions :: OptionMap
getUserSatNum :: REPL SatNum

-- | Get the REPL's string-printer
getPutStr :: REPL (String -> IO ())

-- | Set the REPL's string-printer
setPutStr :: (String -> IO ()) -> REPL ()
smokeTest :: REPL [Smoke]
data Smoke
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 GHC.Base.Functor Cryptol.REPL.Monad.REPL
instance GHC.Base.Applicative Cryptol.REPL.Monad.REPL
instance GHC.Base.Monad Cryptol.REPL.Monad.REPL
instance GHC.Exception.Exception Cryptol.REPL.Monad.REPLException
instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.REPLException
instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.Smoke


module Cryptol.REPL.Command

-- | Commands.
data Command

-- | Successfully parsed command
Command :: (REPL ()) -> Command

-- | Ambiguous command, list of conflicting commands
Ambiguous :: String -> [String] -> Command

-- | The unknown command
Unknown :: String -> Command

-- | Command builder.
data CommandDescr
CommandDescr :: [String] -> CommandBody -> String -> CommandDescr
[cNames] :: CommandDescr -> [String]
[cBody] :: CommandDescr -> CommandBody
[cHelp] :: CommandDescr -> String
data CommandBody
ExprArg :: (String -> REPL ()) -> CommandBody
DeclsArg :: (String -> REPL ()) -> CommandBody
ExprTypeArg :: (String -> REPL ()) -> CommandBody
FilenameArg :: (FilePath -> REPL ()) -> CommandBody
OptionArg :: (String -> REPL ()) -> CommandBody
ShellArg :: (String -> REPL ()) -> CommandBody
NoArg :: (REPL ()) -> CommandBody

-- | Parse a line as a command.
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command

-- | Run a command.
runCommand :: Command -> REPL ()

-- | Split at the first word boundary.
splitCommand :: String -> Maybe (String, String)

-- | Lookup a string in the command list.
findCommand :: String -> [CommandDescr]

-- | Lookup a string in the command list, returning an exact match even if
--   it's the prefix of another command.
findCommandExact :: String -> [CommandDescr]

-- | Lookup a string in the notebook-safe command list.
findNbCommand :: Bool -> String -> [CommandDescr]
moduleCmd :: String -> REPL ()
loadCmd :: FilePath -> REPL ()
loadPrelude :: REPL ()
handleCtrlC :: REPL ()

-- | Strip leading space.
sanitize :: String -> String

-- | Lift a parsing action into the REPL monad.
replParse :: (String -> Either ParseError a) -> String -> REPL a
liftModuleCmd :: ModuleCmd a -> REPL a
moduleCmdResult :: ModuleRes a -> REPL a
instance GHC.Show.Show Cryptol.REPL.Command.QCMode
instance GHC.Classes.Eq Cryptol.REPL.Command.QCMode
instance GHC.Show.Show Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Eq Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Ord Cryptol.REPL.Command.CommandDescr
