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


module Cryptol.Utils.Misc

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

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


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


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


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


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


-- | 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
nEq :: Maybe Nat' -> Maybe Nat' -> Bool
nGt :: Maybe Nat' -> Maybe Nat' -> Bool
nFin :: Maybe Nat' -> Bool
nAdd :: Nat' -> Nat' -> Nat'

-- | Some algebraic 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 algebraic 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'

-- | <tt>length ([ x, y .. ] : [_][w])</tt> We don't check that the second
--   element fits in <tt>w</tt> many bits as the second element may not be
--   part of the list. For example, the length of <tt>[ 0 .. ] :
--   [_][0]</tt> is <tt>nLenFromThen 0 1 0</tt>, which should evaluate to
--   1.
nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'

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

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

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

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

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


module Cryptol.Utils.Ident

-- | Module names are just text.
type ModName = Text
unpackModName :: ModName -> [String]
packModName :: [String] -> ModName
modSep :: Text

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


module Cryptol.Utils.PP

-- | How to display names, inspired by the GHC <tt>Outputable</tt> module.
--   Getting a value of <a>Nothing</a> from the NameDisp function indicates
--   that the name is not in scope.
data NameDisp
EmptyNameDisp :: NameDisp
NameDisp :: (ModName -> Ident -> Maybe NameFormat) -> NameDisp
data NameFormat
UnQualified :: NameFormat
Qualified :: !ModName -> NameFormat
NotInScope :: NameFormat

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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 -> Text -> Position
rComb :: Range -> Range -> Range
rCombs :: [Range] -> Range
class HasLoc t
getLoc :: HasLoc t => t -> Maybe Range
class HasLoc t => AddLoc t
addLoc :: AddLoc t => t -> Range -> t
dropLoc :: AddLoc t => t -> t
at :: (HasLoc l, AddLoc t) => l -> t -> t
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.Position.Located a)
instance GHC.Generics.Generic (Cryptol.Parser.Position.Located a)
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.Position.Located a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.Position.Located a)
instance Control.DeepSeq.NFData Cryptol.Parser.Position.Range
instance GHC.Generics.Generic Cryptol.Parser.Position.Range
instance GHC.Show.Show Cryptol.Parser.Position.Range
instance GHC.Classes.Eq Cryptol.Parser.Position.Range
instance Control.DeepSeq.NFData Cryptol.Parser.Position.Position
instance GHC.Generics.Generic Cryptol.Parser.Position.Position
instance GHC.Show.Show Cryptol.Parser.Position.Position
instance GHC.Classes.Ord Cryptol.Parser.Position.Position
instance GHC.Classes.Eq Cryptol.Parser.Position.Position
instance 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.Utils.PP.PPName a => Cryptol.Utils.PP.PPName (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)


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

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

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

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

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

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

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

-- | keyword
KW :: TokenKW -> TokenT

-- | operator
Op :: TokenOp -> TokenT

-- | symbol
Sym :: TokenSym -> TokenT

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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 -&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
tBinOpPrec :: Map TFun (Assoc, Int)

-- | Type functions, with their arity and function constructor.
tfunNames :: Map PName (Int, TFun)
instance Control.DeepSeq.NFData Cryptol.Prims.Syntax.TFun
instance GHC.Generics.Generic Cryptol.Prims.Syntax.TFun
instance GHC.Enum.Enum Cryptol.Prims.Syntax.TFun
instance GHC.Enum.Bounded Cryptol.Prims.Syntax.TFun
instance GHC.Classes.Ord Cryptol.Prims.Syntax.TFun
instance GHC.Classes.Eq Cryptol.Prims.Syntax.TFun
instance GHC.Show.Show Cryptol.Prims.Syntax.TFun
instance Cryptol.Utils.PP.PPName Cryptol.Prims.Syntax.TFun
instance Cryptol.Utils.PP.PP Cryptol.Prims.Syntax.TFun


module Cryptol.Parser.AST

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

-- | Module names are just text.
type ModName = Text
modRange :: Module name -> Range

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | <pre>
--   (ty)
--   </pre>
TParens :: (Type n) -> Type n

-- | <pre>
--   ty + ty
--   </pre>
TInfix :: (Type n) -> (Located n) -> Fixity -> (Type n) -> Type n
tconNames :: Map PName (Type PName)
data Prop n

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

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

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

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

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

-- | Location information
CLocated :: (Prop n) -> Range -> Prop n

-- | After parsing
CType :: (Type n) -> Prop n
data Module name
Module :: Located ModName -> [Located Import] -> [TopDecl name] -> Module name
[mName] :: Module name -> Located ModName
[mImports] :: Module name -> [Located Import]
[mDecls] :: Module name -> [TopDecl name]
newtype Program name
Program :: [TopDecl name] -> Program name
data TopDecl name
Decl :: (TopLevel (Decl name)) -> TopDecl name
TDNewtype :: (TopLevel (Newtype name)) -> TopDecl name
Include :: (Located FilePath) -> TopDecl name
data Decl name
DSignature :: [Located name] -> (Schema name) -> Decl name
DFixity :: !Fixity -> [Located name] -> Decl name
DPragma :: [Located name] -> Pragma -> Decl name
DBind :: (Bind name) -> Decl name
DPatBind :: (Pattern name) -> (Expr name) -> Decl name
DType :: (TySyn name) -> Decl name
DLocated :: (Decl name) -> Range -> Decl name
data Fixity
Fixity :: !Assoc -> !Int -> Fixity
[fAssoc] :: Fixity -> !Assoc
[fLevel] :: Fixity -> !Int

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

-- | 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 name
Bind :: Located name -> [Pattern name] -> Located (BindDef name) -> Maybe (Schema name) -> Bool -> Maybe Fixity -> [Pragma] -> Bool -> Maybe String -> Bind name

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
data TopLevel a
TopLevel :: ExportType -> Maybe (Located String) -> a -> TopLevel a
[tlExport] :: TopLevel a -> ExportType
[tlDoc] :: TopLevel a -> Maybe (Located String)
[tlValue] :: TopLevel a -> a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | <pre>
--   f x
--   </pre>
EApp :: (Expr n) -> (Expr n) -> Expr n

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

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

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

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

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

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

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

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

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

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

-- | p &lt;- e
Match :: (Pattern name) -> (Expr name) -> Match name
MatchLet :: (Bind name) -> Match name
data Pattern n

-- | <pre>
--   x
--   </pre>
PVar :: (Located n) -> Pattern n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | <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 name => GHC.Show.Show (Cryptol.Parser.AST.Program name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Module name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Module name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Module name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopDecl name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ReplInput name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ReplInput name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.BindDef name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.BindDef name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.BindDef name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.BindDef name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Bind name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Bind name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Bind name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Bind name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Match name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Match name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Match name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Match name)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Expr n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Expr n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Expr n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Expr n)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Decl name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Decl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Decl name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Decl name)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Schema n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Schema n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Schema n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Schema n)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Prop n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Prop n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Prop n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Prop n)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TySyn n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TySyn n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TySyn n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TySyn n)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Newtype name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Newtype name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Newtype name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.Newtype name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TypeInst name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TypeInst name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TypeInst name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.TypeInst name)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Pattern n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Pattern n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Pattern n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Pattern n)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.Type n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Type n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.Type n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.Type n)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Cryptol.Parser.AST.TParam n)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TParam n)
instance GHC.Show.Show n => GHC.Show.Show (Cryptol.Parser.AST.TParam n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Cryptol.Parser.AST.TParam n)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Kind
instance GHC.Generics.Generic Cryptol.Parser.AST.Kind
instance GHC.Show.Show Cryptol.Parser.AST.Kind
instance GHC.Classes.Eq Cryptol.Parser.AST.Kind
instance GHC.Base.Functor Cryptol.Parser.AST.Named
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.Named a)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Named a)
instance Data.Traversable.Traversable Cryptol.Parser.AST.Named
instance Data.Foldable.Foldable Cryptol.Parser.AST.Named
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.Named a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Cryptol.Parser.AST.Named a)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Selector
instance GHC.Generics.Generic Cryptol.Parser.AST.Selector
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 Control.DeepSeq.NFData Cryptol.Parser.AST.Literal
instance GHC.Generics.Generic Cryptol.Parser.AST.Literal
instance GHC.Show.Show Cryptol.Parser.AST.Literal
instance GHC.Classes.Eq Cryptol.Parser.AST.Literal
instance Control.DeepSeq.NFData Cryptol.Parser.AST.NumInfo
instance GHC.Generics.Generic Cryptol.Parser.AST.NumInfo
instance GHC.Show.Show Cryptol.Parser.AST.NumInfo
instance GHC.Classes.Eq Cryptol.Parser.AST.NumInfo
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.ExportSpec name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.ExportSpec name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ExportSpec name)
instance Data.Traversable.Traversable Cryptol.Parser.AST.TopLevel
instance Data.Foldable.Foldable Cryptol.Parser.AST.TopLevel
instance GHC.Base.Functor Cryptol.Parser.AST.TopLevel
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopLevel a)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TopLevel a)
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.Parser.AST.TopLevel a)
instance Control.DeepSeq.NFData Cryptol.Parser.AST.ExportType
instance GHC.Generics.Generic Cryptol.Parser.AST.ExportType
instance GHC.Classes.Ord Cryptol.Parser.AST.ExportType
instance GHC.Show.Show Cryptol.Parser.AST.ExportType
instance GHC.Classes.Eq Cryptol.Parser.AST.ExportType
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Pragma
instance GHC.Generics.Generic Cryptol.Parser.AST.Pragma
instance GHC.Show.Show Cryptol.Parser.AST.Pragma
instance GHC.Classes.Eq Cryptol.Parser.AST.Pragma
instance GHC.Classes.Eq Cryptol.Parser.AST.FixityCmp
instance GHC.Show.Show Cryptol.Parser.AST.FixityCmp
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Fixity
instance GHC.Generics.Generic Cryptol.Parser.AST.Fixity
instance GHC.Show.Show Cryptol.Parser.AST.Fixity
instance GHC.Classes.Eq Cryptol.Parser.AST.Fixity
instance Control.DeepSeq.NFData Cryptol.Parser.AST.Import
instance GHC.Generics.Generic Cryptol.Parser.AST.Import
instance GHC.Show.Show Cryptol.Parser.AST.Import
instance GHC.Classes.Eq Cryptol.Parser.AST.Import
instance Control.DeepSeq.NFData Cryptol.Parser.AST.ImportSpec
instance GHC.Generics.Generic Cryptol.Parser.AST.ImportSpec
instance GHC.Show.Show Cryptol.Parser.AST.ImportSpec
instance GHC.Classes.Eq Cryptol.Parser.AST.ImportSpec
instance GHC.Classes.Ord name => GHC.Base.Monoid (Cryptol.Parser.AST.ExportSpec name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Expr n)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Expr name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Prop name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Prop name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Bind name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Match name)
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Named a)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Schema name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Schema name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Decl name)
instance Cryptol.Parser.Position.AddLoc (Cryptol.Parser.AST.Decl name)
instance Cryptol.Parser.Position.HasLoc a => Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.TopDecl name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Module name)
instance Cryptol.Parser.Position.HasLoc (Cryptol.Parser.AST.Newtype name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Module name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Program name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TopDecl name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Decl name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Newtype name)
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 (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Bind name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.BindDef name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TySyn name)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Literal
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TypeInst name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Expr name)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Selector
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Pattern name)
instance (GHC.Show.Show name, Cryptol.Utils.PP.PPName name) => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Match name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Schema name)
instance Cryptol.Utils.PP.PP Cryptol.Parser.AST.Kind
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.TParam name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Type name)
instance Cryptol.Utils.PP.PPName name => Cryptol.Utils.PP.PP (Cryptol.Parser.AST.Prop name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.Position.Located t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Named t)
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos [t]
instance Cryptol.Parser.AST.NoPos t => Cryptol.Parser.AST.NoPos (GHC.Base.Maybe t)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Program name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Module name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopDecl name)
instance Cryptol.Parser.AST.NoPos a => Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TopLevel a)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Decl name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Newtype name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Bind name)
instance Cryptol.Parser.AST.NoPos Cryptol.Parser.AST.Pragma
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TySyn name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Expr name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TypeInst name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Match name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Pattern name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Schema name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.TParam name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Type name)
instance Cryptol.Parser.AST.NoPos (Cryptol.Parser.AST.Prop name)


module Cryptol.ModuleSystem.Name
data Name

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

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

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

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

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

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

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

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

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

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

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

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

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

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


module Cryptol.TypeCheck.AST

-- | A Cryptol module.
data Module
Module :: !ModName -> ExportSpec Name -> [Import] -> Map Name TySyn -> Map Name Newtype -> [DeclGroup] -> Module
[mName] :: Module -> !ModName
[mExports] :: Module -> ExportSpec Name
[mImports] :: Module -> [Import]
[mTySyns] :: Module -> Map Name TySyn
[mNewtypes] :: Module -> Map Name 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 :: Name -> [TParam] -> [Prop] -> Type -> TySyn

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

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

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

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

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

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

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

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

-- | Name from source, if any.
[tpName] :: TParam -> Maybe Name
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 :: Name -> [Type] -> Type -> Type

-- | Record type
TRec :: [(Ident, 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 :: Name -> Kind -> UserTC
data Expr

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

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

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

-- | Elimination for 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 :: Name -> Expr

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

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

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

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

-- | Proof abstraction. Because we don't keep proofs around we don't need
--   to name the assumption, but we still need to record the assumption.
--   The assumption is the <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 :: Name -> 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 :: !Name -> Schema -> DeclDef -> [Pragma] -> !Bool -> Maybe Fixity -> Maybe String -> Decl
[dName] :: Decl -> !Name
[dSignature] :: Decl -> Schema
[dDefinition] :: Decl -> DeclDef
[dPragmas] :: Decl -> [Pragma]
[dInfix] :: Decl -> !Bool
[dFixity] :: Decl -> Maybe Fixity
[dDoc] :: Decl -> Maybe String
data DeclDef
DPrim :: DeclDef
DExpr :: Expr -> DeclDef
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsNat' :: Type -> Maybe Nat'
tIsNum :: Type -> Maybe Integer
tIsInf :: Type -> Bool
tIsVar :: Type -> Maybe TVar
tIsFun :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsBit :: Type -> Bool
tIsTuple :: Type -> Maybe [Type]
tIsBinFun :: TFun -> Type -> Maybe (Type, Type)

-- | Split up repeated occurances of the given binary type-level function.
tSplitFun :: TFun -> Type -> [Type]
pIsFin :: Prop -> Maybe Type
pIsGeq :: Prop -> Maybe (Type, Type)
pIsEq :: Prop -> Maybe (Type, Type)
pIsArith :: Prop -> Maybe Type
pIsCmp :: Prop -> Maybe Type
pIsNumeric :: Prop -> Bool
tNum :: Integral a => a -> Type
tZero :: Type
tOne :: Type
tTwo :: Type
tInf :: Type
tNat' :: Nat' -> Type
tBit :: Type
tWord :: Type -> Type
tSeq :: Type -> Type -> Type
tChar :: Type
tString :: Int -> Type
tRec :: [(Ident, Type)] -> Type
tTuple :: [Type] -> Type

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

-- | Eliminate outermost 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
infix 4 =#=
(=/=) :: Type -> Type -> Prop
pArith :: Type -> Prop
pCmp :: Type -> Prop

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

-- | 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
infixl 7 .*.

-- | Make addition type.
(.+.) :: Type -> Type -> Type
infixl 6 .+.
(.-.) :: 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

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

-- | Make an expression that is <a>error</a> pre-applied to a type and a
--   message.
eError :: PrimMap -> Type -> String -> Expr
eString :: PrimMap -> String -> Expr
eChar :: PrimMap -> Char -> Expr
class HasKind t
kindOf :: HasKind t => t -> Kind
quickApply :: Kind -> [a] -> Kind
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitAbs :: Expr -> Maybe ((Name, Type), Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
data Name

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

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

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

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

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

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

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

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

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

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

-- | A mapping from an identifier defined in some module to its real name.
data PrimMap
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
[primDecls] :: PrimMap -> Map Ident Name
[primTypes] :: PrimMap -> Map Ident Name
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Module
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Module
instance GHC.Show.Show Cryptol.TypeCheck.AST.Module
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Match
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Match
instance GHC.Show.Show Cryptol.TypeCheck.AST.Match
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Decl
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Decl
instance GHC.Show.Show Cryptol.TypeCheck.AST.Decl
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclGroup
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclGroup
instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclGroup
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Expr
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Expr
instance GHC.Show.Show Cryptol.TypeCheck.AST.Expr
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.DeclDef
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.DeclDef
instance GHC.Show.Show Cryptol.TypeCheck.AST.DeclDef
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Schema
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Schema
instance GHC.Show.Show Cryptol.TypeCheck.AST.Schema
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.Schema
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.TySyn
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.TySyn
instance GHC.Show.Show Cryptol.TypeCheck.AST.TySyn
instance GHC.Classes.Eq Cryptol.TypeCheck.AST.TySyn
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Newtype
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Newtype
instance GHC.Show.Show Cryptol.TypeCheck.AST.Newtype
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Type
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Type
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 Control.DeepSeq.NFData Cryptol.TypeCheck.AST.TCon
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.TCon
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 Control.DeepSeq.NFData Cryptol.TypeCheck.AST.TC
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.TC
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 Control.DeepSeq.NFData Cryptol.TypeCheck.AST.UserTC
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.UserTC
instance GHC.Show.Show Cryptol.TypeCheck.AST.UserTC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.PC
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.PC
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 Control.DeepSeq.NFData Cryptol.TypeCheck.AST.TVar
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.TVar
instance GHC.Show.Show Cryptol.TypeCheck.AST.TVar
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.TParam
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.TParam
instance GHC.Show.Show Cryptol.TypeCheck.AST.TParam
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Kind
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Kind
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.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.PP.WithNames Cryptol.TypeCheck.AST.DeclDef)
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.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 (Nat', TValue)
isTFun :: TValue -> Maybe (TValue, TValue)
isTTuple :: TValue -> Maybe (Int, [TValue])
isTRec :: TValue -> Maybe [(Ident, TValue)]
tvSeq :: Nat' -> TValue -> TValue
finNat' :: Nat' -> Integer

-- | width, value Invariant: The value must be within the range 0 ..
--   2^width-1
data BV
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 :: [(Ident, 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
VNumPoly :: (Nat' -> GenValue b w) -> GenValue b w
type Value = GenValue Bool BV

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

-- | <ul>
--   <li><i>inf</i> t</li>
--   </ul>
TVStream :: TValue -> TValue
TVTuple :: [TValue] -> TValue
TVRec :: [(Ident, TValue)] -> TValue
TVFun :: TValue -> TValue -> 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> of kind *.
tlam :: (TValue -> GenValue b w) -> GenValue b w

-- | A type lambda that expects a <tt>Type</tt> of kind #.
nlam :: (Nat' -> 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 :: Nat' -> 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 :: Nat' -> 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.
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 polymorphic function from a value.
fromVNumPoly :: GenValue b w -> (Nat' -> 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 -> [(Ident, GenValue b w)]

-- | Lookup a field in a record.
lookupRecord :: Ident -> 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 :: PrimMap -> Type -> Value -> Maybe Expr
instance GHC.Base.Functor Cryptol.Eval.Value.WithBase
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Value.GenValue b w)
instance GHC.Generics.Generic (Cryptol.Eval.Value.GenValue b w)
instance Control.DeepSeq.NFData Cryptol.Eval.Value.TValue
instance GHC.Generics.Generic Cryptol.Eval.Value.TValue
instance Control.DeepSeq.NFData Cryptol.Eval.Value.BV
instance GHC.Generics.Generic Cryptol.Eval.Value.BV
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


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 of kind *. These types do not contain type
--   variables, type synonyms, or type functions.
data TValue
TVBit :: TValue
TVSeq :: Integer -> TValue -> TValue

-- | <ul>
--   <li><i>inf</i> t</li>
--   </ul>
TVStream :: TValue -> TValue
TVTuple :: [TValue] -> TValue
TVRec :: [(Ident, TValue)] -> TValue
TVFun :: TValue -> TValue -> TValue
isTBit :: TValue -> Bool
tvSeq :: Nat' -> TValue -> TValue

-- | Generic value type, parameterized by bit and word types.
data GenValue b w
VRecord :: [(Ident, 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
VNumPoly :: (Nat' -> 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> of kind *.
tlam :: (TValue -> GenValue b w) -> GenValue b w

-- | A type lambda that expects a <tt>Type</tt> of kind #.
nlam :: (Nat' -> 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 :: Nat' -> TValue -> [GenValue b w] -> GenValue b w
finNat' :: Nat' -> Integer

-- | 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 polymorphic function from a value.
fromVNumPoly :: GenValue b w -> (Nat' -> 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 -> [(Ident, GenValue b w)]

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

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

-- | Extract a packed 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


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

-- | Apply a substitution. Returns <a>Nothing</a> if nothing changed.
apSubstMaybe :: Subst -> Type -> Maybe Type
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.DeclDef
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module


module Cryptol.TypeCheck.Sanity
tcExpr :: Map Name Schema -> Expr -> Either Error (Schema, [ProofObligation])
tcDecls :: Map Name Schema -> [DeclGroup] -> Either Error [ProofObligation]
tcModule :: Map Name Schema -> Module -> Either Error [ProofObligation]
type ProofObligation = Schema
data Error

-- | expected, actual
TypeMismatch :: Schema -> Schema -> Error

-- | expected a mono type, got this
ExpectedMono :: Schema -> Error
TupleSelectorOutOfRange :: Int -> Int -> Error
MissingField :: Ident -> [Ident] -> Error
UnexpectedTupleShape :: Int -> Int -> Error
UnexpectedRecordShape :: [Ident] -> [Ident] -> Error
UnexpectedSequenceShape :: Int -> Type -> Error
BadSelector :: Selector -> Type -> Error
BadInstantiation :: Error
Captured :: TVar -> Error
BadProofNoAbs :: Error
BadProofTyVars :: [TParam] -> Error
KindMismatch :: Kind -> Kind -> Error
NotEnoughArgumentsInKind :: Kind -> Error
BadApplication :: Type -> Type -> Error
FreeTypeVariable :: TVar -> Error
BadTypeApplication :: Kind -> [Kind] -> Error
RepeatedVariableInForall :: TParam -> Error
BadMatch :: Type -> Error
EmptyArm :: Error
UndefinedTypeVaraible :: TVar -> Error
UndefinedVariable :: Name -> Error
same :: Same a => a -> a -> Bool
instance GHC.Show.Show Cryptol.TypeCheck.Sanity.Error
instance Cryptol.TypeCheck.Sanity.Same a => Cryptol.TypeCheck.Sanity.Same [a]
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.AST.Type
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.AST.Schema
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.AST.TParam
instance GHC.Base.Functor Cryptol.TypeCheck.Sanity.TcM
instance GHC.Base.Applicative Cryptol.TypeCheck.Sanity.TcM
instance GHC.Base.Monad Cryptol.TypeCheck.Sanity.TcM


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


-- | The sytnax of numeric propositions.
module Cryptol.TypeCheck.Solver.Numeric.AST
data Name
UserName :: TVar -> Name
SysName :: Int -> Name

-- | Pretty print a name.
ppName :: Name -> Doc

-- | Propopsitions, representing Cryptol's numeric constraints (and a bit
--   more).
data Prop
Fin :: Expr -> Prop
(:==) :: Expr -> Expr -> Prop
(:>=) :: Expr -> Expr -> Prop
(:>) :: Expr -> Expr -> Prop
(:==:) :: Expr -> Expr -> Prop
(:>:) :: Expr -> Expr -> Prop
(:&&) :: Prop -> Prop -> Prop
(:||) :: Prop -> Prop -> Prop
Not :: Prop -> Prop
PFalse :: Prop
PTrue :: Prop

-- | Compute all expressions in a property.
cryPropExprs :: Prop -> [Expr]

-- | Compute the free variables in a proposition.
cryPropFVS :: Prop -> Set Name

-- | Pretty print a top-level property.
ppProp :: Prop -> Doc

-- | Pretty print a proposition, in the given precedence context.
ppPropPrec :: Int -> Prop -> Doc

-- | Expressions, representing Cryptol's numeric types.
data Expr
K :: Nat' -> 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
Width :: Expr -> Expr
LenFromThen :: Expr -> Expr -> Expr -> Expr
LenFromThenTo :: Expr -> Expr -> Expr -> Expr

-- | The constant <tt>0</tt>.
zero :: Expr

-- | The constant <tt>1</tt>.
one :: Expr

-- | The constant <tt>2</tt>.
two :: Expr

-- | The constant <tt>infinity</tt>.
inf :: Expr

-- | Make a conjucntion of the given properties.
cryAnds :: [Prop] -> Prop

-- | Make a disjunction of the given properties.
cryOrs :: [Prop] -> Prop

-- | Compute the immediate sub-expressions of an expression.
cryExprExprs :: Expr -> [Expr]

-- | Rebuild an expression, using the top-level strucutre of the first
--   expression, but the second list of expressions as sub-expressions.
cryRebuildExpr :: Expr -> [Expr] -> Expr

-- | Compute the free variables in an expression.
cryExprFVS :: Expr -> Set Name

-- | Pretty print an expression at the top level.
ppExpr :: Expr -> Doc

-- | Pretty print an expression, in the given precedence context.
ppExprPrec :: Int -> Expr -> Doc

-- | Natural numbers with an infinity element
data Nat'
Nat :: Integer -> Nat'
Inf :: Nat'
type IfExpr = IfExpr' Prop
data IfExpr' p a
If :: p -> (IfExpr' p a) -> (IfExpr' p a) -> IfExpr' p a
Return :: a -> IfExpr' p a
Impossible :: IfExpr' p a

-- | Pretty print an experssion with ifs.
ppIf :: (p -> Doc) -> (a -> Doc) -> IfExpr' p a -> Doc

-- | Pretty print an experssion with ifs.
ppIfExpr :: IfExpr Expr -> Doc
type Subst = Map Name Expr

-- | Replaces occurances of the name with the expression. Returns
--   <a>Nothing</a> if there were no occurances of the name.
class HasVars ast
apSubst :: HasVars ast => Subst -> ast -> Maybe ast
cryLet :: HasVars e => Name -> Expr -> e -> Maybe e
composeSubst :: Subst -> Subst -> Subst
doAppSubst :: HasVars a => Subst -> a -> a
instance (GHC.Classes.Eq p, GHC.Classes.Eq a) => GHC.Classes.Eq (Cryptol.TypeCheck.Solver.Numeric.AST.IfExpr' p a)
instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.Numeric.AST.Prop
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.AST.Prop
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.AST.Prop
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.Numeric.AST.Expr
instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.Numeric.AST.Expr
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.AST.Expr
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.AST.Expr
instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.Numeric.AST.Name
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.Numeric.AST.Name
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.AST.Name
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.AST.Name
instance GHC.Base.Monad (Cryptol.TypeCheck.Solver.Numeric.AST.IfExpr' p)
instance GHC.Base.Functor (Cryptol.TypeCheck.Solver.Numeric.AST.IfExpr' p)
instance GHC.Base.Applicative (Cryptol.TypeCheck.Solver.Numeric.AST.IfExpr' p)
instance Cryptol.TypeCheck.Solver.Numeric.AST.HasVars GHC.Types.Bool
instance Cryptol.TypeCheck.Solver.Numeric.AST.HasVars Cryptol.TypeCheck.Solver.Numeric.AST.Expr
instance Cryptol.TypeCheck.Solver.Numeric.AST.HasVars Cryptol.TypeCheck.Solver.Numeric.AST.Prop


-- | Simplification of expressions. The result of simplifying an expression
--   <tt>e</tt>, is a new expression <tt>e'</tt>, which satisfies the
--   property:
--   
--   if e is well-defined then e and e' will evaluate to the same type.
module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr

-- | Simplify an expression, if possible.
crySimpExpr :: Expr -> Expr

-- | Perform simplification from the leaves up. Returns <a>Nothing</a> if
--   there were no changes.
crySimpExprMaybe :: Expr -> Maybe Expr
data Sign
Pos :: Sign
Neg :: Sign
otherSign :: Sign -> Sign
signed :: Sign -> Integer -> Integer
splitSum :: Expr -> [(Sign, Expr)]
normSum :: Expr -> Expr
crySimpExprStep :: Expr -> Maybe Expr

-- | Make a simplification step, assuming the expression is well-formed.
crySimpExprStep1 :: Expr -> Maybe Expr
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr.Sign


-- | Simplification. The rules in this module are all conditional on the
--   expressions being well-defined.
--   
--   So, for example, consider the formula <tt>P</tt>, which corresponds to
--   `fin e`. <tt>P</tt> says the following:
--   
--   if e is well-formed, then will evaluate to a finite natural number.
--   
--   More concretely, consider `fin (3 - 5)`. This will be simplified to
--   <a>True</a>, which does not mean that `3 - 5` is actually finite.
module Cryptol.TypeCheck.Solver.Numeric.Simplify1
propToProp' :: Prop -> I Bool
ppProp' :: I Bool -> Doc
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.Numeric.Simplify1.Atom
instance (GHC.Classes.Eq a, Cryptol.TypeCheck.Solver.Numeric.AST.HasVars a) => Cryptol.TypeCheck.Solver.Numeric.AST.HasVars (Cryptol.TypeCheck.Solver.Numeric.Simplify1.I a)


module Cryptol.TypeCheck.Solver.Numeric.Defined

-- | A condition ensure that the given *basic* proposition makes sense.
cryDefinedProp :: Prop -> Prop

-- | Generate a property ensuring that the expression is well-defined. This
--   might be a bit too strict. For example, we reject things like <tt>max
--   inf (0 - 1)</tt>, which one might think would simplify to
--   <tt>inf</tt>.
cryDefined :: Expr -> Prop


-- | TODO: - Putting in a normal form to spot "prove by assumption" -
--   Additional simplification rules, namely various cancelation. - Things
--   like: lg2 e(x) = x, where we know thate is increasing.
module Cryptol.TypeCheck.Solver.Numeric.Simplify

-- | Simplify a property, if possible.
crySimplify :: Prop -> Prop

-- | Simplify a property, if possible.
crySimplifyMaybe :: Prop -> Maybe Prop

-- | Simplify only the Expr parts of a Prop.
crySimpPropExpr :: Prop -> Prop

-- | Simplify only the Expr parts of a Prop. Returns <a>Nothing</a> if
--   there were no changes.
crySimpPropExprMaybe :: Prop -> Maybe Prop


-- | Separate Non-Linear Constraints When we spot a non-linear expression,
--   we name it and add it to a map.
--   
--   If we see the same expression multiple times, then we give it the same
--   name.
--   
--   The body of the non-linear expression is not processed further, so the
--   resulting map should not contain any of the newly minted names.
module Cryptol.TypeCheck.Solver.Numeric.NonLin

-- | Factor-out non-linear terms, by naming them.
nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS)
data NonLinS

-- | Get the known non-linear terms.
nonLinSubst :: NonLinS -> Subst

-- | The initial state for the linearization process.
initialNonLinS :: NonLinS

-- | Apply a substituin to the non-linear expression database. Returns
--   <a>Nothing</a> if nothing was affected. Otherwise returns <a>Just</a>,
--   and a substitution for non-linear expressions that became linear.
--   
--   The definitions of NL terms do not contain other named NL terms, so it
--   does not matter if the substitution contains bindings like <tt>_a =
--   e</tt>.
--   
--   There should be no bindings that mention NL term names in the
--   definitions of the substition (i.e, things like <tt>x = _a</tt> are
--   NOT ok).
apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS)
lookupNL :: Name -> NonLinS -> Maybe Expr
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Numeric.NonLin.NonLinS


module Cryptol.TypeCheck.Solver.Numeric.ImportExport
type ExportM = ExceptionT () Id
exportProp :: Prop -> Maybe Prop
exportType :: Prop -> Maybe Expr
runExportM :: ExportM a -> Maybe a
exportPropM :: Prop -> ExportM Prop
exportTypeM :: Type -> ExportM Expr
importProp :: Prop -> Maybe [Prop]
importType :: Expr -> Maybe Type


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

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

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

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

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

-- | Returns <a>True</a> when the intervals definitely overlap, and
--   <a>False</a> otherwise.
iDisjoint :: Interval -> Interval -> Bool

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

-- | Any value
iAny :: Interval

-- | Any finite value
iAnyFin :: Interval

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


module Cryptol.TypeCheck.TypeOf

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


module Cryptol.TypeCheck.Solver.Utils

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


-- | Desugar into SMTLIB Terminology
module Cryptol.TypeCheck.Solver.Numeric.SMT

-- | Assumes simplified, linear, defined.
desugarProp :: Prop -> IfExpr Prop

-- | The name of a variable in the SMT translation.
smtName :: Name -> String

-- | The name of a boolean variable, representing `fin x`.
smtFinName :: Name -> String
ifPropToSmtLib :: IfExpr Prop -> SExpr

-- | Given a model, compute an improving substitution, implied by the
--   model. The entries in the substitution look like this:
--   
--   <ul>
--   <li><tt>x = A</tt> variable <tt>x</tt> must equal constant
--   <tt>A</tt></li>
--   <li><tt>x = y</tt> variable <tt>x</tt> must equal variable
--   <tt>y</tt></li>
--   <li><tt>x = A * y + B</tt> (coming soon) variable <tt>x</tt> is a
--   linear function of <tt>y</tt>, <tt>A</tt> and <tt>B</tt> are natural
--   numbers.</li>
--   </ul>
--   
--   We are mostly interested in improving unification variables. However,
--   it is also useful to improve skolem variables, as this could turn
--   non-linear constraints into linear ones. For example, if we have a
--   constraint <tt>x * y = z</tt>, and we can figure out that <tt>x</tt>
--   must be 5, then we end up with a linear constraint <tt>5 * y = z</tt>.
cryImproveModel :: Solver -> Logger -> Map Name Nat' -> IO (Map Name Expr, [Prop])

-- | Get the value for the given name. * Assumes that we are in a SAT state
--   (i.e., there is a model) * Assumes that the name is in the model
getVal :: Solver -> Name -> IO Nat'

-- | Get the values for the given names.
getVals :: Solver -> [Name] -> IO (Map Name Nat')


module Cryptol.Testing.Concrete

-- | 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
isPass :: TestResult -> Bool

-- | Apply a testable value to some arguments. Note that this function
--   assumes that the values come from a call to <a>testableType</a> (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

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

-- | 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]
data TestSpec m s
TestSpec :: (Integer -> s -> m (TestResult, s)) -> String -> Integer -> Integer -> (Integer -> Integer -> m ()) -> m () -> (TestResult -> m ()) -> m () -> TestSpec m s
[testFn] :: TestSpec m s -> Integer -> s -> m (TestResult, s)

-- | The property as entered by the user
[testProp] :: TestSpec m s -> String
[testTotal] :: TestSpec m s -> Integer
[testPossible] :: TestSpec m s -> Integer
[testRptProgress] :: TestSpec m s -> Integer -> Integer -> m ()
[testClrProgress] :: TestSpec m s -> m ()
[testRptFailure] :: TestSpec m s -> TestResult -> m ()
[testRptSuccess] :: TestSpec m s -> m ()
data TestReport
TestReport :: TestResult -> String -> Integer -> Integer -> TestReport
[reportResult] :: TestReport -> TestResult

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


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 Name IfaceTySyn -> Map Name IfaceNewtype -> Map Name IfaceDecl -> IfaceDecls
[ifTySyns] :: IfaceDecls -> Map Name IfaceTySyn
[ifNewtypes] :: IfaceDecls -> Map Name IfaceNewtype
[ifDecls] :: IfaceDecls -> Map Name IfaceDecl
type IfaceTySyn = TySyn
ifTySynName :: TySyn -> Name
type IfaceNewtype = Newtype
data IfaceDecl
IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl
[ifDeclName] :: IfaceDecl -> !Name
[ifDeclSig] :: IfaceDecl -> Schema
[ifDeclPragmas] :: IfaceDecl -> [Pragma]
[ifDeclInfix] :: IfaceDecl -> Bool
[ifDeclFixity] :: IfaceDecl -> Maybe Fixity
[ifDeclDoc] :: IfaceDecl -> Maybe String
mkIfaceDecl :: Decl -> IfaceDecl

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

-- | Produce a PrimMap from an interface.
--   
--   NOTE: the map will expose <i>both</i> public and private names.
ifacePrimMap :: Iface -> PrimMap
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.Iface
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.Iface
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.Iface
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecls
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecls
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Interface.IfaceDecl
instance GHC.Generics.Generic Cryptol.ModuleSystem.Interface.IfaceDecl
instance GHC.Show.Show Cryptol.ModuleSystem.Interface.IfaceDecl
instance 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 :: Supply -> Module -> (Module, Supply)
instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.Transform.MonoValues.RewMap' (Cryptol.ModuleSystem.Name.Name, [Cryptol.TypeCheck.AST.Type], GHC.Types.Int)


module Cryptol.Eval.Env
type ReadEnv = EvalEnv
data EvalEnv
EvalEnv :: Map Name Value -> Map TVar (Either Nat' TValue) -> EvalEnv
[envVars] :: EvalEnv -> Map Name Value
[envTypes] :: EvalEnv -> Map TVar (Either Nat' TValue)
emptyEnv :: EvalEnv

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

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

-- | Bind a type variable of kind # or *.
bindType :: TVar -> Either Nat' TValue -> EvalEnv -> EvalEnv

-- | Lookup a type variable.
lookupType :: TVar -> EvalEnv -> Maybe (Either Nat' TValue)
instance Control.DeepSeq.NFData Cryptol.Eval.Env.EvalEnv
instance GHC.Generics.Generic Cryptol.Eval.Env.EvalEnv
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 (kind * or #).
evalType :: EvalEnv -> Type -> Either Nat' TValue

-- | Evaluation for value types (kind *).
evalValType :: EvalEnv -> Type -> TValue
evalNumType :: EvalEnv -> Type -> Nat'

-- | Reduce type functions, raising an exception for undefined values.
evalTF :: TFun -> [Nat'] -> Nat'


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


-- | The purpose of this module is to convert all patterns to variable
--   patterns. It also eliminates pattern bindings by de-sugaring them into
--   <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 :: PName -> [Located (Schema PName)] -> Error
SignatureNoBind :: (Located PName) -> (Schema PName) -> Error
PragmaNoBind :: (Located PName) -> Pragma -> Error
MultipleFixities :: PName -> [Range] -> Error
FixityNoBind :: (Located PName) -> Error
MultipleDocs :: PName -> [Range] -> Error
instance Control.DeepSeq.NFData Cryptol.Parser.NoPat.Error
instance GHC.Generics.Generic Cryptol.Parser.NoPat.Error
instance GHC.Show.Show Cryptol.Parser.NoPat.Error
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Program Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Expr Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName]
instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM
instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error


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

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

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

-- | Expression-level fixity environment
[neFixity] :: NamingEnv -> !(Map Name Fixity)

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

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

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

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

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

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

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

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

-- | Generate a <a>NamingEnv</a> using an explicit supply.
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply)
newtype BuildNamingEnv
BuildNamingEnv :: SupplyT Id NamingEnv -> BuildNamingEnv
[runBuild] :: BuildNamingEnv -> SupplyT Id NamingEnv

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

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

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

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

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

-- | Introduce the name

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

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

-- | The naming environment for a single declaration.
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.ModuleSystem.NamingEnv.InModule a)
instance Data.Foldable.Foldable Cryptol.ModuleSystem.NamingEnv.InModule
instance Data.Traversable.Traversable Cryptol.ModuleSystem.NamingEnv.InModule
instance GHC.Base.Functor Cryptol.ModuleSystem.NamingEnv.InModule
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Generics.Generic Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Show.Show Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance GHC.Base.Monoid Cryptol.ModuleSystem.NamingEnv.BuildNamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.NamingEnv
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames (GHC.Base.Maybe a)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames a => Cryptol.ModuleSystem.NamingEnv.BindsNames [a]
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Schema Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames Cryptol.ModuleSystem.NamingEnv.ImportIface
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Bind Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.TParam Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName)
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.TopDecl Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Newtype Cryptol.Parser.Name.PName))
instance Cryptol.ModuleSystem.NamingEnv.BindsNames (Cryptol.ModuleSystem.NamingEnv.InModule (Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName))


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

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

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

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

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

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

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

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

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

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

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

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

-- | The goal can never be solved.
Unsolvable :: Solved
data Warning
DefaultingKind :: (TParam Name) -> 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 result (which should not be of the
--   form <tt>_ -&gt; _</tt>)
TooManyTypeParams :: Int -> Kind -> Error

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

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

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

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

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

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

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

-- | Attempt to explicitly instantiate a non-existent param.
UndefinedTypeParam :: (Located Ident) -> Error

-- | Multiple definitions for the same type parameter
MultipleTypeParamDefs :: Ident -> [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 The boolean indicates if we know
--   that this constraint is impossible.
UnsolvedGoal :: Bool -> Goal -> Error

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

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

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

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

-- | The given constraints causes the signature of the function to be
--   not-satisfiable.
UnusableFunction :: Name -> [Prop] -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
AmbiguousType :: [Name] -> 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 expression
CtInst :: Expr -> ConstraintSource
CtSelector :: ConstraintSource
CtExactType :: ConstraintSource
CtEnumeration :: ConstraintSource

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

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

-- | Constraints arising from type-checking patterns
CtPattern :: Doc -> ConstraintSource
data TyFunName
UserTyFun :: Name -> 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 Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.Error
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.Error
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Error
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.DelayedCt
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Solved
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Goal
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.ConstraintSource
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.ConstraintSource
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.ConstraintSource
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.TyFunName
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.TyFunName
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.TyFunName
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.Warning
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.Warning
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.Warning
instance Control.DeepSeq.NFData Cryptol.TypeCheck.InferTypes.SolverConfig
instance GHC.Generics.Generic Cryptol.TypeCheck.InferTypes.SolverConfig
instance GHC.Show.Show Cryptol.TypeCheck.InferTypes.SolverConfig
instance Cryptol.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


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

-- | Solve class constraints. If not, then we return <a>Nothing</a>. If
--   solved, ther we return <a>Just</a> a list of sub-goals.
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]


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


module Cryptol.TypeCheck.Solver.CrySAT

-- | Execute a computation in a new solver scope.
withScope :: Solver -> IO a -> IO a

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

-- | Add the given constraints as assumptions. * We assume that the
--   constraints are well-defined. * Modifies the set of assumptions.
assumeProps :: Solver -> [Prop] -> IO [SimpProp]

-- | Simplify a bunch of well-defined properties. * Eliminates properties
--   that are implied by the rest. * Does not modify the set of
--   assumptions.
simplifyProps :: Solver -> [DefinedProp Goal] -> IO [Goal]

-- | Attempt to find a substituion that, when applied, makes all of the
--   given properties hold.
getModel :: Solver -> [Prop] -> IO (Maybe Subst)

-- | Check if the current set of assumptions is satisfiable, and find some
--   facts that must hold in any models of the current assumptions.
--   
--   Returns <a>Nothing</a> if the currently asserted constraints are known
--   to be unsatisfiable.
--   
--   Returns `Just (su, sub-goals)` is the current set is satisfiable. *
--   The <tt>su</tt> is a substitution that may be applied to the current
--   constraint set without loosing generality. * The `sub-goals` are
--   additional constraints that must hold if the constraint set is to be
--   satisfiable.
check :: Solver -> IO (Maybe (Subst, [Prop]))

-- | An SMT solver, and some info about declared variables.
data Solver

-- | For debugging
logger :: Solver -> Logger
getIntervals :: Solver -> IO (Either TVar (Map TVar Interval))

-- | <a>dpSimpProp</a> and <a>dpSimpExprProp</a> should be logically
--   equivalent, to each other, and to whatever <tt>a</tt> represents
--   (usually <tt>a</tt> is a <a>Goal</a>).
data DefinedProp a
DefinedProp :: a -> SimpProp -> Prop -> DefinedProp a

-- | Optional data to associate with prop. Often, the original <a>Goal</a>
--   from which the prop was extracted.
[dpData] :: DefinedProp a -> a

-- | Fully simplified: may mention ORs, and named non-linear terms. These
--   are what we send to the prover, and we don't attempt to convert them
--   back into Cryptol types.
[dpSimpProp] :: DefinedProp a -> SimpProp

-- | A version of the proposition where just the expression terms have been
--   simplified. These should not contain ORs or named non-linear terms
--   because we want to import them back into Crytpol types.
[dpSimpExprProp] :: DefinedProp a -> Prop
debugBlock :: Solver -> String -> IO a -> IO a
class DebugLog t where debugLogList s ts = case ts of { [] -> debugLog s "(none)" _ -> mapM_ (debugLog s) ts }
debugLog :: DebugLog t => Solver -> t -> IO ()
debugLogList :: DebugLog t => Solver -> [t] -> IO ()
knownDefined :: (a, Prop) -> DefinedProp a

-- | Class goals go on the left, numeric goals go on the right.
numericRight :: Goal -> Either Goal (Goal, Prop)

-- | Given a list of propositions that together lead to a contradiction,
--   find a sub-set that still leads to a contradiction (but is smaller).
minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a]
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.VarInfo
instance GHC.Show.Show Cryptol.TypeCheck.Solver.CrySAT.Scope
instance Cryptol.TypeCheck.Solver.CrySAT.HasProp Cryptol.TypeCheck.AST.Prop
instance Cryptol.TypeCheck.Solver.CrySAT.HasProp Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog GHC.Types.Char
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog a => Cryptol.TypeCheck.Solver.CrySAT.DebugLog [a]
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog a => Cryptol.TypeCheck.Solver.CrySAT.DebugLog (GHC.Base.Maybe a)
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog Cryptol.Utils.PP.Doc
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog Cryptol.TypeCheck.AST.Type
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog Cryptol.TypeCheck.Subst.Subst
instance Cryptol.TypeCheck.Solver.CrySAT.DebugLog Cryptol.TypeCheck.Solver.Numeric.AST.Prop


module Cryptol.TypeCheck.Monad

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> NameSeeds -> Bool -> SolverConfig -> !PrimMap -> !Supply -> InferInput

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

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

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

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

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

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

-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig

-- | The mapping from <tt>Ident</tt> to <a>Name</a>, for names that the
--   typechecker needs to refer to.
[inpPrimNames] :: InferInput -> !PrimMap

-- | The supply for fresh name generation
[inpSupply] :: InferInput -> !Supply

-- | 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 -> Supply -> 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 Name VarType -> [TParam] -> Map Name (DefLoc, TySyn) -> Map Name (DefLoc, Newtype) -> Map Int (Expr -> Expr) -> Bool -> Solver -> !PrimMap -> RO

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

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

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

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

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

-- | 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
[iSolver] :: RO -> Solver
[iPrimNames] :: RO -> !PrimMap

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

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

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

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

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

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

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

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

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

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

-- | Report an error.
recordError :: Error -> InferM ()
recordWarning :: Warning -> InferM ()
getSolver :: InferM Solver

-- | Retrieve the mapping between identifiers and declarations in the
--   prelude.
getPrimMap :: InferM PrimMap
newGoal :: ConstraintSource -> Prop -> InferM Goal

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

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

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

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

-- | 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 Name -> 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 :: Name -> 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 :: Name -> InferM (Maybe Type)

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

-- | Lookup the definition of a newtype
lookupNewtype :: Name -> 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 :: Name -> Kind -> InferM Type

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

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

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

-- | Return the keys of the bound variables that are in scope.
getBoundInScope :: InferM (Set 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 -> Name -> InferM ()

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

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

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

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

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

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

-- | Perform the given computation in a new scope (i.e., the subcomputation
--   may use existential type variables).
inNewScope :: InferM a -> InferM a
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 Name Type -> Bool -> KRO

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

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

-- | kinds of (known) vars.
[typeParams] :: KRW -> Map Name 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 -> [(Name, Maybe Kind, Type)] -> KindM a -> InferM (a, Map Name 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 :: Name -> 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 :: Name -> KindM (Maybe TySyn)

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

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

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

-- | The sub-computation is about the given range of the source code.
kInRange :: Range -> KindM a -> KindM a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kInInferM :: InferM a -> KindM a
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.Monad.InferOutput a)
instance GHC.Show.Show Cryptol.TypeCheck.Monad.InferInput
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Generics.Generic Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Show.Show Cryptol.TypeCheck.Monad.NameSeeds
instance GHC.Base.Functor Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Applicative Cryptol.TypeCheck.Monad.InferM
instance GHC.Base.Monad Cryptol.TypeCheck.Monad.InferM
instance Control.Monad.Fix.MonadFix Cryptol.TypeCheck.Monad.InferM
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.TypeCheck.Monad.InferM
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 Name) -> TyDecl
NT :: (Newtype Name) -> TyDecl

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

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

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

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

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

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


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


module Cryptol.TypeCheck.Solver.Selector

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


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


module Cryptol.Parser
parseModule :: Config -> Text -> Either ParseError (Module PName)
parseProgram :: Layout -> Text -> Either ParseError (Program PName)
parseProgramWith :: Config -> Text -> Either ParseError (Program PName)
parseExpr :: Text -> Either ParseError (Expr PName)
parseExprWith :: Config -> Text -> Either ParseError (Expr PName)
parseDecl :: Text -> Either ParseError (Decl PName)
parseDeclWith :: Config -> Text -> Either ParseError (Decl PName)
parseDecls :: Text -> Either ParseError [Decl PName]
parseDeclsWith :: Config -> Text -> Either ParseError [Decl PName]
parseLetDecl :: Text -> Either ParseError (Decl PName)
parseLetDeclWith :: Config -> Text -> Either ParseError (Decl PName)
parseRepl :: Text -> Either ParseError (ReplInput PName)
parseReplWith :: Config -> Text -> Either ParseError (ReplInput PName)
parseSchema :: Text -> Either ParseError (Schema PName)
parseSchemaWith :: Config -> Text -> Either ParseError (Schema PName)
parseModName :: String -> Maybe ModName
parseHelpName :: String -> Maybe PName
data ParseError
HappyError :: FilePath -> 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
removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
data IncludeError
IncludeFailed :: (Located FilePath) -> IncludeError
IncludeParseError :: ParseError -> IncludeError
IncludeCycle :: [Located FilePath] -> IncludeError
ppIncludeError :: IncludeError -> Doc
instance Control.DeepSeq.NFData Cryptol.Parser.NoInclude.IncludeError
instance GHC.Generics.Generic Cryptol.Parser.NoInclude.IncludeError
instance GHC.Show.Show Cryptol.Parser.NoInclude.IncludeError
instance GHC.Base.Functor Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Applicative Cryptol.Parser.NoInclude.NoIncM
instance GHC.Base.Monad Cryptol.Parser.NoInclude.NoIncM


module Cryptol.ModuleSystem.Renamer
data NamingEnv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | When a builtin type is named in a binder.
BoundReservedType :: PName -> (Maybe Range) -> Doc -> NameDisp -> RenamerError
data RenamerWarning
SymbolShadowed :: Name -> [Name] -> NameDisp -> RenamerWarning
renameVar :: PName -> RenameM Name
renameType :: PName -> RenameM Name
renameModule :: Module PName -> RenameM (NamingEnv, Module Name)
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.EnvCheck
instance GHC.Classes.Eq Cryptol.ModuleSystem.Renamer.EnvCheck
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerWarning
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Renamer.RenamerError
instance GHC.Generics.Generic Cryptol.ModuleSystem.Renamer.RenamerError
instance GHC.Show.Show Cryptol.ModuleSystem.Renamer.RenamerError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerError
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Renamer.RenamerWarning
instance GHC.Base.Monoid a => GHC.Base.Monoid (Cryptol.ModuleSystem.Renamer.RenameM a)
instance GHC.Base.Functor Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Applicative Cryptol.ModuleSystem.Renamer.RenameM
instance GHC.Base.Monad Cryptol.ModuleSystem.Renamer.RenameM
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.ModuleSystem.Renamer.RenameM
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TopDecl
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Decl
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Newtype
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Schema
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TParam
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Prop
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Type
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Bind
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.BindDef
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Pattern
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Expr
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TypeInst
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.Match
instance Cryptol.ModuleSystem.Renamer.Rename Cryptol.Parser.AST.TySyn


module Cryptol.TypeCheck.Solver.Simplify

-- | When given an equality constraint, attempt to rewrite it to the form
--   `?x = ...`, by moving all occurrences of `?x` to the LHS, and any
--   other variables to the RHS. This will only work when there's only one
--   unification variable present in the prop.
tryRewritePropAsSubst :: Map TVar Interval -> Prop -> Maybe (TVar, Type)


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

-- | Add additional constraints that ensure the validity of a type.
wfType :: Type -> [Prop]

-- | Add additional constraints that ensure validity of type function. Note
--   that these constraints do not introduce additional malformed types, so
--   the well-formedness constraints are guaranteed to be well-formed. This
--   assumes that the parameters are well-formed.
wfTypeFunction :: TFun -> [Type] -> [Prop]
improveByDefaultingWith :: Solver -> [TVar] -> [Goal] -> IO ([TVar], [Goal], Subst, [Warning])

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


-- | This module generates random values for Cryptol types.
module Cryptol.Testing.Random
type Gen g = Integer -> 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] -> Integer -> g -> IO (TestResult, g)

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

-- | 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 => [(Ident, Gen g)] -> Gen g


module Cryptol.Prims.Eval
evalPrim :: Decl -> Value
primTable :: Map Ident 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 :: Nat' -> Nat' -> TValue -> Value -> Value
splitAtV :: Nat' -> Nat' -> 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 :: Nat' -> Nat' -> 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 -> Integer -> Integer) -> (Nat' -> TValue -> [Value] -> Integer -> [Value]) -> Value
shiftLW :: Integer -> Integer -> Integer -> Integer
shiftLS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
shiftRW :: Integer -> Integer -> Integer -> Integer
shiftRS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
rotateLW :: Integer -> Integer -> Integer -> Integer
rotateLS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
rotateRW :: Integer -> Integer -> Integer -> Integer
rotateRS :: Nat' -> TValue -> [Value] -> Integer -> [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


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
instance GHC.Base.Functor Cryptol.Eval.ZList
instance GHC.Base.Applicative Cryptol.Eval.ZList
instance GHC.Base.Monoid Cryptol.Eval.ListEnv


module Cryptol.Symbolic.Prims
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
evalPrim :: Decl -> Value
primTable :: Map Ident Value
selectV :: (Integer -> Value) -> Value -> Value
asWordList :: [Value] -> Maybe [SWord]
atV_list :: Bool -> Bool -> Value -> [Value] -> Value -> Value
atV :: Bool -> Value -> [Value] -> Value -> Value
iteAtV :: Value -> [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
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 :: Nat' -> Nat' -> 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.TypeCheck.Kind
checkType :: Type Name -> Maybe Kind -> InferM Type

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

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

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


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

-- | Construct a primitive in the parsed AST.
mkPrim :: String -> InferM (Expr Name)
desugarLiteral :: Bool -> Literal -> InferM (Expr Name)

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

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

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

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

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

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

-- | Infer the type of one arm of a list comprehension.
inferCArm :: Int -> [Match Name] -> InferM ([Match], Map Name (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 Name] -> 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 Name Expr -> Bind Name -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))

-- | Try to evaluate the inferred type in a binding.
simpBind :: Decl -> Decl

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


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

-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> NameSeeds -> Bool -> SolverConfig -> !PrimMap -> !Supply -> InferInput

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

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

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

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

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

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

-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig

-- | The mapping from <tt>Ident</tt> to <a>Name</a>, for names that the
--   typechecker needs to refer to.
[inpPrimNames] :: InferInput -> !PrimMap

-- | The supply for fresh name generation
[inpSupply] :: InferInput -> !Supply

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

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

-- | Type inference was successful.
InferOK :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
data SolverConfig
SolverConfig :: FilePath -> [String] -> Int -> SolverConfig

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

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

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

-- | 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 result (which should not be of the
--   form <tt>_ -&gt; _</tt>)
TooManyTypeParams :: Int -> Kind -> Error

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

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

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

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

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

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

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

-- | Attempt to explicitly instantiate a non-existent param.
UndefinedTypeParam :: (Located Ident) -> Error

-- | Multiple definitions for the same type parameter
MultipleTypeParamDefs :: Ident -> [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 The boolean indicates if we know
--   that this constraint is impossible.
UnsolvedGoal :: Bool -> Goal -> Error

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

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

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

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

-- | The given constraints causes the signature of the function to be
--   not-satisfiable.
UnusableFunction :: Name -> [Prop] -> Error

-- | Too many positional type arguments, in an explicit type instantiation
TooManyPositionalTypeParams :: Error
CannotMixPositionalAndNamedTypeParams :: Error
AmbiguousType :: [Name] -> Error
data Warning
DefaultingKind :: (TParam Name) -> 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 -> SolverConfig -> CoreLint -> !Supply -> ModuleEnv
[meLoadedModules] :: ModuleEnv -> LoadedModules
[meNameSeeds] :: ModuleEnv -> NameSeeds
[meEvalEnv] :: ModuleEnv -> EvalEnv
[meFocusedModule] :: ModuleEnv -> Maybe ModName
[meSearchPath] :: ModuleEnv -> [FilePath]
[meDynEnv] :: ModuleEnv -> DynamicEnv
[meMonoBinds] :: ModuleEnv -> !Bool
[meSolverConfig] :: ModuleEnv -> SolverConfig
[meCoreLint] :: ModuleEnv -> CoreLint
[meSupply] :: ModuleEnv -> !Supply
data CoreLint

-- | Don't run core lint
NoCoreLint :: CoreLint

-- | Run core lint
CoreLint :: CoreLint
resetModuleEnv :: ModuleEnv -> ModuleEnv
initialModuleEnv :: IO ModuleEnv

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

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

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system, as well as a <a>NameDisp</a> for pretty-printing names
--   according to the imports.
--   
--   XXX This could really do with some better error handling, just
--   returning mempty when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)

-- | The unqualified declarations and name environment for the dynamic
--   environment.
dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)

-- | Retrieve all <a>IfaceDecls</a> referenced by a module, as well as all
--   of its public and private declarations, checking expressions
qualifiedEnv :: ModuleEnv -> 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 Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.ModuleEnv
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.ModuleEnv
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.DynamicEnv
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.DynamicEnv
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModules
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModules
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.LoadedModule
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.LoadedModule
instance GHC.Show.Show Cryptol.ModuleSystem.Env.LoadedModule
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Env.CoreLint
instance GHC.Generics.Generic Cryptol.ModuleSystem.Env.CoreLint
instance 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
getSupply :: ModuleM Supply
getMonoBinds :: ModuleM Bool
setMonoBinds :: Bool -> ModuleM ()
setNameSeeds :: NameSeeds -> ModuleM ()
setSupply :: Supply -> 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, NamingEnv, NameDisp)
getQualifiedEnv :: ModuleM IfaceDecls
getDynEnv :: ModuleM DynamicEnv
setDynEnv :: DynamicEnv -> ModuleM ()
setSolver :: SolverConfig -> ModuleM ()
getSolverConfig :: ModuleM SolverConfig
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleWarning
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ModuleError
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Generics.Generic Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Show.Show Cryptol.ModuleSystem.Monad.ImportSource
instance GHC.Classes.Eq Cryptol.ModuleSystem.Monad.ImportSource
instance Cryptol.Utils.PP.PP Cryptol.ModuleSystem.Monad.ImportSource
instance Control.DeepSeq.NFData Cryptol.ModuleSystem.Monad.ModuleError
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
instance GHC.Base.Monad m => Cryptol.ModuleSystem.Name.FreshM (Cryptol.ModuleSystem.Monad.ModuleT m)


module Cryptol.ModuleSystem.Base
rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a

-- | Rename a module in the context of its imported modules.
renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)

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

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

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

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

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

-- | Find the interface referenced by an import, and generate the naming
--   environment that it describes.
importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)

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

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

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

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

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

-- | Load the local environment, which consists of the environment for the
--   currently opened module, shadowed by the dynamic environment.
getLocalEnv :: ModuleM (IfaceDecls, NamingEnv)

-- | Typecheck a single expression, yielding a renamed parsed expression,
--   typechecked core expression, and a type schema.
checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema)

-- | Typecheck a group of declarations.
--   
--   INVARIANT: This assumes that NoPat has already been run on the
--   declarations.
checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])

-- | Generate the primitive map. If the prelude is currently being loaded,
--   this should be generated directly from the naming environment given to
--   the renamer instead.
getPrimMap :: ModuleM PrimMap

-- | Typecheck a module.
checkModule :: FilePath -> Module PName -> ModuleM Module
data TCLinter o
TCLinter :: (o -> InferInput -> Either Error [ProofObligation]) -> Maybe ModName -> TCLinter o
[lintCheck] :: TCLinter o -> o -> InferInput -> Either Error [ProofObligation]
[lintModule] :: TCLinter o -> Maybe ModName
exprLinter :: TCLinter (Expr, Schema)
declsLinter :: TCLinter [DeclGroup]
moduleLinter :: ModName -> TCLinter Module
data TCAction i o
TCAction :: (i -> InferInput -> IO (InferOutput o)) -> TCLinter o -> PrimMap -> TCAction i o
[tcAction] :: TCAction i o -> i -> InferInput -> IO (InferOutput o)
[tcLinter] :: TCAction i o -> TCLinter o
[tcPrims] :: TCAction i o -> PrimMap
typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceDecls -> ModuleM o

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


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

-- | Extra information we need to carry around to dynamically extend an
--   environment outside the context of a single module. Particularly
--   useful when dealing with interactive declarations as in <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 PName -> ModuleCmd Module

-- | Check the type of an expression. Give back the renamed expression, the
--   core expression, and its type schema.
checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)

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

-- | Typecheck top-level declarations.
checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])

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

-- | Produce an ifaceDecls that represents the focused environment of the
--   module system, as well as a <a>NameDisp</a> for pretty-printing names
--   according to the imports.
--   
--   XXX This could really do with some better error handling, just
--   returning mempty when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
getPrimMap :: ModuleCmd PrimMap
renameVar :: NamingEnv -> PName -> ModuleCmd Name
renameType :: NamingEnv -> PName -> ModuleCmd Name

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

-- | Generate an Iface from a typechecked module.
genIface :: Module -> Iface
type IfaceTySyn = TySyn
data IfaceDecl
IfaceDecl :: !Name -> Schema -> [Pragma] -> Bool -> Maybe Fixity -> Maybe String -> IfaceDecl
[ifDeclName] :: IfaceDecl -> !Name
[ifDeclSig] :: IfaceDecl -> Schema
[ifDeclPragmas] :: IfaceDecl -> [Pragma]
[ifDeclInfix] :: IfaceDecl -> Bool
[ifDeclFixity] :: IfaceDecl -> Maybe Fixity
[ifDeclDoc] :: IfaceDecl -> Maybe String


module Cryptol.Transform.Specialize

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

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

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

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

-- | Compute the specialization of `EWhere e dgs`. A decl within
--   <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 Name (TypesMap Name))
specializeConst :: Expr -> SpecM Expr
destEProofApps :: Expr -> (Expr, Int)
destETApps :: Expr -> (Expr, [Type])
destEProofAbs :: Expr -> ([Prop], Expr)
destETAbs :: Expr -> ([TParam], Expr)

-- | Freshen a name by giving it a new unique.
freshName :: Name -> [Type] -> SpecM Name
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema

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


module Cryptol.Symbolic
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 :: [(Ident, FinType)] -> FinType
numType :: Integer -> Maybe Int
finType :: TValue -> Maybe FinType
unFinType :: FinType -> Type
predArgTypes :: Schema -> Either String [FinType]
forallFinType :: FinType -> Symbolic Value
existsFinType :: FinType -> Symbolic Value
data Env
Env :: Map Name Value -> Map TVar (Either Nat' TValue) -> Env
[envVars] :: Env -> Map Name Value
[envTypes] :: Env -> Map TVar (Either Nat' TValue)

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

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

-- | Bind a type variable of kind *.
bindType :: TVar -> (Either Nat' TValue) -> Env -> Env

-- | Lookup a type variable.
lookupType :: TVar -> Env -> Maybe (Either Nat' TValue)
evalExpr :: Env -> Expr -> Value
evalValType :: Env -> Type -> TValue
evalNumType :: Env -> Type -> Nat'
evalSel :: Selector -> Value -> Value
evalDecls :: Env -> [DeclGroup] -> Env
evalDeclGroup :: Env -> DeclGroup -> Env
evalDecl :: Env -> Decl -> (Name, 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 :: NameDisp -> ModuleError -> REPLException
EvalPolyError :: Schema -> REPLException
TypeNotTestable :: Type -> REPLException
rethrowEvalError :: IO a -> IO a
getFocusedEnv :: REPL (IfaceDecls, NamingEnv, NameDisp)
getModuleEnv :: REPL ModuleEnv
setModuleEnv :: ModuleEnv -> REPL ()
getDynEnv :: REPL DynamicEnv
setDynEnv :: DynamicEnv -> REPL ()

-- | Given an existing qualified name, prefix it with a relatively-unique
--   string. We make it unique by prefixing with a character <tt>#</tt>
--   that is not lexically valid in a module name.
uniqify :: Name -> REPL Name

-- | Generate a fresh name using the given index. The name will reside
--   within the "<a>interactive</a>" namespace.
freshName :: Ident -> REPL Name
getTSyns :: REPL (Map Name TySyn)
getNewtypes :: REPL (Map Name Newtype)
getVars :: REPL (Map Name IfaceDecl)
whenDebug :: REPL () -> REPL ()

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

-- | Get visible type signature names.
getTypeNames :: REPL [String]

-- | Return a list of property names, sorted by position in the file.
getPropertyNames :: REPL ([Name], NameDisp)
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 ()

-- | 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
EnvProg :: String -> [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 Control.Monad.IO.Class.MonadIO Cryptol.REPL.Monad.REPL
instance Control.Monad.Base.MonadBase GHC.Types.IO Cryptol.REPL.Monad.REPL
instance Control.Monad.Trans.Control.MonadBaseControl GHC.Types.IO Cryptol.REPL.Monad.REPL
instance Cryptol.ModuleSystem.Name.FreshM Cryptol.REPL.Monad.REPL
instance GHC.Exception.Exception Cryptol.REPL.Monad.REPLException
instance Cryptol.Utils.PP.PP Cryptol.REPL.Monad.REPLException
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
FileExprArg :: (FilePath -> 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 ()
setOptionCmd :: String -> REPL ()
interactiveConfig :: Config
replParseExpr :: String -> REPL (Expr PName)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)

-- | Randomly test a property, or exhaustively check it if the number of
--   values in the type under test is smaller than the <tt>tests</tt>
--   environment variable, or we specify exhaustive testing.
qcCmd :: QCMode -> String -> REPL [TestReport]
data QCMode
QCRandom :: QCMode
QCExhaust :: QCMode
satCmd :: String -> REPL ()
proveCmd :: String -> REPL ()
onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL ProverResult
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
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