-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Cryptol: The Language of Cryptography
--
-- Cryptol is a domain-specific language for specifying cryptographic
-- algorithms. A Cryptol implementation of an algorithm resembles its
-- mathematical specification more closely than an implementation in a
-- general purpose language. For more, see
-- http://www.cryptol.net/.
@package cryptol
@version 2.5.0
module Cryptol.Version
commitHash :: String
commitShortHash :: String
commitBranch :: String
commitDirty :: Bool
version :: Version
module Cryptol.Utils.Patterns
newtype Match b
Match :: (forall r. r -> (b -> r) -> r) -> Match b
type Pat a b = a -> Match b
(|||) :: Pat a b -> Pat a b -> Pat a b
-- | Check that a value satisfies multiple patterns. For example, an "as"
-- pattern is (__ &&& p).
(&&&) :: Pat a b -> Pat a c -> Pat a (b, c)
-- | Match a value, and modify the result.
(~>) :: Pat a b -> (b -> c) -> Pat a c
-- | Match a value, and return the given result
(~~>) :: Pat a b -> c -> Pat a c
-- | View pattern.
(<~) :: (a -> b) -> Pat b c -> Pat a c
-- | Variable pattern.
__ :: Pat a a
-- | Constant pattern.
succeed :: a -> Pat x a
-- | Predicate pattern
checkThat :: (a -> Bool) -> Pat a ()
-- | Check for exact value.
lit :: Eq a => a -> Pat a ()
-- | Match a pattern, using the given default if valure.
matchDefault :: a -> Match a -> a
-- | Match an irrefutable pattern. Crashes on faliure.
match :: Match a -> a
matchMaybe :: Match a -> Maybe a
list :: [Pat a b] -> Pat [a] [b]
(><) :: Pat a b -> Pat x y -> Pat (a, x) (b, y)
class Matches thing pats res | pats -> thing res
matches :: Matches thing pats res => thing -> pats -> Match res
instance GHC.Base.Functor Cryptol.Utils.Patterns.Match
instance GHC.Base.Applicative Cryptol.Utils.Patterns.Match
instance GHC.Base.Monad Cryptol.Utils.Patterns.Match
instance GHC.Base.Alternative Cryptol.Utils.Patterns.Match
instance GHC.Base.MonadPlus Cryptol.Utils.Patterns.Match
instance (f ~ Cryptol.Utils.Patterns.Pat a a1', a1 ~ Cryptol.Utils.Patterns.Pat a1' r1) => Cryptol.Utils.Patterns.Matches a (f, a1) r1
instance (op ~ Cryptol.Utils.Patterns.Pat a (a1', a2'), a1 ~ Cryptol.Utils.Patterns.Pat a1' r1, a2 ~ Cryptol.Utils.Patterns.Pat a2' r2) => Cryptol.Utils.Patterns.Matches a (op, a1, a2) (r1, r2)
instance (op ~ Cryptol.Utils.Patterns.Pat a (a1', a2', a3'), a1 ~ Cryptol.Utils.Patterns.Pat a1' r1, a2 ~ Cryptol.Utils.Patterns.Pat a2' r2, a3 ~ Cryptol.Utils.Patterns.Pat a3' r3) => Cryptol.Utils.Patterns.Matches a (op, a1, a2, a3) (r1, r2, r3)
module Cryptol.Utils.Panic
panic :: String -> [String] -> a
instance GHC.Show.Show Cryptol.Utils.Panic.CryptolPanic
instance GHC.Exception.Exception Cryptol.Utils.Panic.CryptolPanic
module Cryptol.Utils.Misc
-- | Apply a function to all elements of a container. Returns
-- Nothing if nothing changed, and Just container
-- otherwise.
anyJust :: Traversable t => (a -> Maybe a) -> t a -> Maybe (t a)
-- | Apply functions to both elements of a pair. Returns Nothing if
-- neither changed, and Just pair otherwise.
anyJust2 :: (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
module Cryptol.Utils.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
preludeExtrasName :: 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 Outputable module.
-- Getting a value of Nothing 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 Nothing is returned, the name
-- is not currently in scope.
getNameFormat :: ModName -> Ident -> NameDisp -> NameFormat
-- | Produce a document in the context of the current NameDisp.
withNameDisp :: (NameDisp -> Doc) -> Doc
-- | Fix the way that names are displayed inside of a doc.
fixNameDisp :: NameDisp -> Doc -> Doc
newtype Doc
Doc :: (NameDisp -> Doc) -> Doc
runDoc :: NameDisp -> Doc -> Doc
render :: Doc -> String
class PP a
ppPrec :: PP a => Int -> a -> Doc
class PP a => PPName a
-- | Fixity information for infix operators
ppNameFixity :: PPName a => a -> Maybe (Assoc, Int)
-- | Print a name in prefix: f a b or (+) a b)
ppPrefixName :: PPName a => a -> Doc
-- | Print a name as an infix operator: a + b
ppInfixName :: PPName a => a -> Doc
pp :: PP a => a -> Doc
pretty :: PP a => a -> String
optParens :: Bool -> Doc -> Doc
-- | Information about associativity.
data Assoc
LeftAssoc :: Assoc
RightAssoc :: Assoc
NonAssoc :: Assoc
-- | Information about an infix expression of some sort.
data Infix op thing
Infix :: op -> thing -> thing -> Int -> Assoc -> Infix op thing
-- | operator
[ieOp] :: Infix op thing -> op
-- | left argument
[ieLeft] :: Infix op thing -> thing
-- | right 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.Utils.Debug
trace :: String -> b -> b
ppTrace :: Doc -> b -> b
-- | This module defines natural numbers with an additional infinity
-- element, and various arithmetic operators on them.
module Cryptol.TypeCheck.Solver.InfNat
-- | Natural numbers with an infinity element
data Nat'
Nat :: Integer -> Nat'
Inf :: Nat'
fromNat :: Nat' -> Maybe Integer
nAdd :: Nat' -> Nat' -> Nat'
-- | Some algebraic properties of interest:
--
--
-- 1 * x = x
-- x * (y * z) = (x * y) * z
-- 0 * x = 0
-- x * y = y * x
-- x * (a + b) = x * a + x * b
--
nMul :: Nat' -> Nat' -> Nat'
-- | Some algebraic properties of interest:
--
--
-- x ^ 0 = 1
-- x ^ (n + 1) = x * (x ^ n)
-- x ^ (m + n) = (x ^ m) * (x ^ n)
-- x ^ (m * n) = (x ^ m) ^ n
--
nExp :: Nat' -> Nat' -> Nat'
nMin :: Nat' -> Nat' -> Nat'
nMax :: Nat' -> Nat' -> Nat'
-- | nSub x y = Just z iff z is the unique value such
-- that Add y z = Just x.
nSub :: Nat' -> Nat' -> Maybe Nat'
-- | Rounds down.
--
--
-- y * q + r = x
-- x / y = q with remainder r
-- 0 <= r && r < y
--
--
-- We don't allow Inf in the first argument for two reasons: 1. It
-- matches the behavior of nMod, 2. The well-formedness
-- constraints can be expressed as a conjunction.
nDiv :: Nat' -> Nat' -> Maybe Nat'
nMod :: Nat' -> Nat' -> Maybe Nat'
-- | Rounds up. lg2 x = y, iff y is the smallest number
-- such that x <= 2 ^ y
nLg2 :: Nat' -> Nat'
-- | nWidth n is number of bits needed to represent all numbers
-- from 0 to n, inclusive. nWidth x = nLg2 (x + 1).
nWidth :: Nat' -> Nat'
-- | length ([ x, y .. ] : [_][w]) We don't check that the second
-- element fits in w many bits as the second element may not be
-- part of the list. For example, the length of [ 0 .. ] :
-- [_][0] is nLenFromThen 0 1 0, which should evaluate to
-- 1.
nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'
-- |
-- length [ x, y .. z ]
--
nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'
-- | Compute the logarithm of a number in the given base, rounded down to
-- the closest integer. The boolean indicates if we the result is exact
-- (i.e., True means no rounding happened, False means we rounded down).
-- The logarithm base is the second argument.
genLog :: Integer -> Integer -> Maybe (Integer, Bool)
-- | Compute the number of bits required to represent the given integer.
widthInteger :: Integer -> Integer
-- | Compute the exact root of a natural number. The second argument
-- specifies which root we are computing.
rootExact :: Integer -> Integer -> Maybe Integer
-- | Compute the the n-th root of a natural number, rounded down to the
-- closest natural number. The boolean indicates if the result is exact
-- (i.e., True means no rounding was done, False means rounded down). The
-- second argument specifies which root we are computing.
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Generics.Generic Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Classes.Ord Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Classes.Eq Cryptol.TypeCheck.Solver.InfNat.Nat'
instance GHC.Show.Show Cryptol.TypeCheck.Solver.InfNat.Nat'
module Cryptol.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.REPL.Trie
-- | Maps string names to values, allowing for partial key matches and
-- querying.
data Trie a
Node :: (Map Char (Trie a)) -> (Maybe a) -> Trie a
emptyTrie :: Trie a
-- | Insert a value into the Trie. Will call panic if a value
-- already exists with that key.
insertTrie :: String -> a -> Trie a -> Trie a
-- | Return all matches with the given prefix.
lookupTrie :: String -> Trie a -> [a]
-- | Given a key, return either an exact match for that key, or all matches
-- with the given prefix.
lookupTrieExact :: String -> Trie a -> [a]
-- | Return all of the values from a Trie.
leaves :: Trie a -> [a]
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.REPL.Trie.Trie a)
-- | Convert a literate source file into an ordinary source file.
module Cryptol.Parser.Unlit
unLit :: PreProc -> Text -> Text
data PreProc
None :: PreProc
Markdown :: PreProc
LaTeX :: PreProc
guessPreProc :: FilePath -> PreProc
knownExts :: [String]
module Cryptol.Parser.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)
module Cryptol.Parser.Name
-- | Names that originate in the parser.
data PName
-- | Unqualified names like x, Foo, or +.
UnQual :: !Ident -> PName
-- | Qualified names like Foo::bar or module::!.
Qual :: !ModName -> !Ident -> PName
-- | Fresh names generated by a pass.
NewName :: !Pass -> !Int -> PName
-- | Passes that can generate fresh names.
data Pass
NoPat :: Pass
MonoValues :: Pass
mkUnqual :: Ident -> PName
mkQual :: ModName -> Ident -> PName
getModName :: PName -> Maybe ModName
getIdent :: PName -> Ident
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
-- |
-- : Num -> Num -> Num
--
TCAdd :: TFun
-- |
-- : Num -> Num -> Num
--
TCSub :: TFun
-- |
-- : Num -> Num -> Num
--
TCMul :: TFun
-- |
-- : Num -> Num -> Num
--
TCDiv :: TFun
-- |
-- : Num -> Num -> Num
--
TCMod :: TFun
-- |
-- : Num -> Num -> Num
--
TCExp :: TFun
-- |
-- : Num -> Num
--
TCWidth :: TFun
-- |
-- : Num -> Num -> Num
--
TCMin :: TFun
-- |
-- : Num -> Num -> Num
--
TCMax :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. ]
-- :: [lengthFromThen 1 5 b][b]
TCLenFromThen :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9
-- ] :: [lengthFromThenTo 1 5 9][b]
TCLenFromThenTo :: TFun
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
-- | 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
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 x, Foo, or +.
UnQual :: !Ident -> PName
-- | Qualified names like Foo::bar or module::!.
Qual :: !ModName -> !Ident -> PName
-- | Fresh names generated by a pass.
NewName :: !Pass -> !Int -> PName
getModName :: PName -> Maybe ModName
getIdent :: PName -> Ident
mkUnqual :: Ident -> PName
mkQual :: ModName -> Ident -> PName
data Named a
Named :: Located Ident -> a -> Named a
[name] :: Named a -> Located Ident
[value] :: Named a -> a
-- | Passes that can generate fresh names.
data Pass
NoPat :: Pass
MonoValues :: Pass
-- | Information about associativity.
data Assoc
LeftAssoc :: Assoc
RightAssoc :: Assoc
NonAssoc :: Assoc
data Schema n
Forall :: [TParam n] -> [Prop n] -> (Type n) -> (Maybe Range) -> Schema n
data TParam n
TParam :: n -> Maybe Kind -> Maybe Range -> TParam n
[tpName] :: TParam n -> n
[tpKind] :: TParam n -> Maybe Kind
[tpRange] :: TParam n -> Maybe Range
data Kind
KNum :: Kind
KType :: Kind
data Type n
-- |
-- [8] -> [8]
--
TFun :: (Type n) -> (Type n) -> Type n
-- |
-- [8] a
--
TSeq :: (Type n) -> (Type n) -> Type n
-- |
-- Bit
--
TBit :: Type n
-- |
-- 10
--
TNum :: Integer -> Type n
-- |
-- a
--
TChar :: Char -> Type n
-- |
-- inf
--
TInf :: Type n
-- | A type variable or synonym
TUser :: n -> [Type n] -> Type n
-- |
-- 2 + x
--
TApp :: TFun -> [Type n] -> Type n
-- |
-- { x : [8], y : [32] }
--
TRecord :: [Named (Type n)] -> Type n
-- |
-- ([8], [32])
--
TTuple :: [Type n] -> Type n
-- | _, just some type.
TWild :: Type n
-- | Location information
TLocated :: (Type n) -> Range -> Type n
-- |
-- (ty)
--
TParens :: (Type n) -> Type n
-- |
-- ty + ty
--
TInfix :: (Type n) -> (Located n) -> Fixity -> (Type n) -> Type n
tconNames :: Map PName (Type PName)
data Prop n
-- |
-- fin x
--
CFin :: (Type n) -> Prop n
-- |
-- x == 10
--
CEqual :: (Type n) -> (Type n) -> Prop n
-- |
-- x >= 10
--
CGeq :: (Type n) -> (Type n) -> Prop n
-- |
-- Arith a
--
CArith :: (Type n) -> Prop n
-- |
-- Cmp a
--
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:
--
--
-- - The parser does not associate type signatures and pragmas with
-- their bindings: this is done in a separate pass, after de-sugaring
-- pattern bindings. In this way we can associate pragmas and type
-- signatures with the variables defined by pattern bindings as
-- well.
-- - Currently, there is no surface syntax for defining monomorphic
-- bindings (i.e., bindings that will not be automatically generalized by
-- the type checker. However, they are useful when de-sugaring
-- patterns.
--
data Bind name
Bind :: Located name -> [Pattern name] -> Located (BindDef name) -> Maybe (Schema name) -> Bool -> Maybe Fixity -> [Pragma] -> Bool -> Maybe String -> Bind name
-- | Defined thing
[bName] :: Bind name -> Located name
-- | Parameters
[bParams] :: Bind name -> [Pattern name]
-- | Definition
[bDef] :: Bind name -> Located (BindDef name)
-- | Optional type sig
[bSignature] :: Bind name -> Maybe (Schema name)
-- | Infix operator?
[bInfix] :: Bind name -> Bool
-- | Optional fixity info
[bFixity] :: Bind name -> Maybe Fixity
-- | Optional pragmas
[bPragmas] :: Bind name -> [Pragma]
-- | Is this a monomorphic binding
[bMono] :: Bind name -> Bool
-- | Optional doc string
[bDoc] :: Bind name -> Maybe String
data BindDef name
DPrim :: BindDef name
DExpr :: (Expr name) -> BindDef name
type LBindDef = Located (BindDef PName)
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma
-- | Export information for a declaration.
data ExportType
Public :: ExportType
Private :: ExportType
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 Name entries in the list are expected
-- to be unqualified names; the QName or NewName
-- constructors should not be present.
data ImportSpec
Hiding :: [Ident] -> ImportSpec
Only :: [Ident] -> ImportSpec
data Newtype name
Newtype :: Located name -> [TParam name] -> [Named (Type name)] -> Newtype name
-- | Type name
[nName] :: Newtype name -> Located name
-- | Type params
[nParams] :: Newtype name -> [TParam name]
-- | Constructor
[nBody] :: Newtype name -> [Named (Type name)]
-- | Input at the REPL, which can either be an expression or a let
-- statement.
data ReplInput name
ExprInput :: (Expr name) -> ReplInput name
LetInput :: (Decl name) -> ReplInput name
data Expr n
-- |
-- x
--
EVar :: n -> Expr n
-- |
-- 0x10
--
ELit :: Literal -> Expr n
-- |
-- (1,2,3)
--
ETuple :: [Expr n] -> Expr n
-- |
-- { x = 1, y = 2 }
--
ERecord :: [Named (Expr n)] -> Expr n
-- |
-- e.l
--
ESel :: (Expr n) -> Selector -> Expr n
-- |
-- [1,2,3]
--
EList :: [Expr n] -> Expr n
-- |
-- [1, 5 .. 117 ]
--
EFromTo :: (Type n) -> (Maybe (Type n)) -> (Maybe (Type n)) -> Expr n
-- |
-- [1, 3 ...]
--
EInfFrom :: (Expr n) -> (Maybe (Expr n)) -> Expr n
-- |
-- [ 1 | x <- xs ]
--
EComp :: (Expr n) -> [[Match n]] -> Expr n
-- |
-- f x
--
EApp :: (Expr n) -> (Expr n) -> Expr n
-- |
-- f `{x = 8}, f`{8}
--
EAppT :: (Expr n) -> [(TypeInst n)] -> Expr n
-- |
-- if ok then e1 else e2
--
EIf :: (Expr n) -> (Expr n) -> (Expr n) -> Expr n
-- |
-- 1 + x where { x = 2 }
--
EWhere :: (Expr n) -> [Decl n] -> Expr n
-- |
-- 1 : [8]
--
ETyped :: (Expr n) -> (Type n) -> Expr n
-- | `(x + 1), x is a type
ETypeVal :: (Type n) -> Expr n
-- |
-- \x y -> x
--
EFun :: [Pattern n] -> (Expr n) -> Expr n
-- | position annotation
ELocated :: (Expr n) -> Range -> Expr n
-- | (e) (Removed by Fixity)
EParens :: (Expr n) -> Expr n
-- | a + b (Removed by Fixity)
EInfix :: (Expr n) -> (Located n) -> Fixity -> (Expr n) -> Expr n
-- | Literals.
data Literal
-- | 0x10 (HexLit 2)
ECNum :: Integer -> NumInfo -> Literal
-- |
-- "hello"
--
ECString :: String -> Literal
-- | Infromation about the representation of a numeric constant.
data NumInfo
-- | n-digit binary literal
BinLit :: Int -> NumInfo
-- | n-digit octal literal
OctLit :: Int -> NumInfo
-- | overloaded decimal literal
DecLit :: NumInfo
-- | n-digit hex literal
HexLit :: Int -> NumInfo
-- | character literal
CharLit :: NumInfo
-- | polynomial literal
PolyLit :: Int -> NumInfo
data Match name
-- | p <- e
Match :: (Pattern name) -> (Expr name) -> Match name
MatchLet :: (Bind name) -> Match name
data Pattern n
-- |
-- x
--
PVar :: (Located n) -> Pattern n
-- |
-- _
--
PWild :: Pattern n
-- |
-- (x,y,z)
--
PTuple :: [Pattern n] -> Pattern n
-- |
-- { x = (a,b,c), y = z }
--
PRecord :: [Named (Pattern n)] -> Pattern n
-- |
-- [ x, y, z ]
--
PList :: [Pattern n] -> Pattern n
-- |
-- x : [8]
--
PTyped :: (Pattern n) -> (Type n) -> Pattern n
-- |
-- (x # y)
--
PSplit :: (Pattern n) -> (Pattern n) -> Pattern n
-- | Location information
PLocated :: (Pattern n) -> Range -> Pattern n
-- | Selectors are used for projecting from various components. Each
-- selector has an option spec to specify the shape of the thing that is
-- being selected. Currently, there is no surface syntax for list
-- selectors, but they are used during the desugaring of patterns.
data Selector
-- | Zero-based tuple selection. Optionally specifies the shape of the
-- tuple (one-based).
TupleSel :: Int -> (Maybe Int) -> Selector
-- | Record selection. Optionally specifies the shape of the record.
RecordSel :: Ident -> (Maybe [Ident]) -> Selector
-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> (Maybe Int) -> Selector
data TypeInst name
NamedInst :: (Named (Type name)) -> TypeInst name
PosInst :: (Type name) -> TypeInst name
data Located a
Located :: !Range -> !a -> Located a
[srcRange] :: Located a -> !Range
[thing] :: Located a -> !a
-- | A name with location information.
type LPName = Located PName
-- | A string with location information.
type LString = Located String
-- | An identifier with location information.
type LIdent = Located Ident
class NoPos t
noPos :: NoPos t => t -> t
-- | Conversational printing of kinds (e.g., to use in error
-- messages)
cppKind :: Kind -> Doc
-- | Display the thing selected by the selector, nicely.
ppSelector :: Selector -> Doc
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Program name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.Module name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.Module name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.Module name)
instance Control.DeepSeq.NFData name => Control.DeepSeq.NFData (Cryptol.Parser.AST.TopDecl name)
instance GHC.Generics.Generic (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.TopDecl name)
instance GHC.Show.Show name => GHC.Show.Show (Cryptol.Parser.AST.ReplInput name)
instance GHC.Classes.Eq name => GHC.Classes.Eq (Cryptol.Parser.AST.ReplInput name)
instance 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)
-- | 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
-- x 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
-- Bind. Furthermore, here we associate signatures and pragmas
-- with the names to which they belong.
module Cryptol.Parser.NoPat
class RemovePatterns t
-- | Eliminate all patterns in a program.
removePatterns :: RemovePatterns t => t -> (t, [Error])
data Error
MultipleSignatures :: PName -> [Located (Schema PName)] -> Error
SignatureNoBind :: (Located PName) -> (Schema PName) -> Error
PragmaNoBind :: (Located PName) -> Pragma -> Error
MultipleFixities :: PName -> [Range] -> Error
FixityNoBind :: (Located PName) -> Error
MultipleDocs :: PName -> [Range] -> Error
instance Control.DeepSeq.NFData Cryptol.Parser.NoPat.Error
instance GHC.Generics.Generic Cryptol.Parser.NoPat.Error
instance GHC.Show.Show Cryptol.Parser.NoPat.Error
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Program Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Expr Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns (Cryptol.Parser.AST.Module Cryptol.Parser.Name.PName)
instance Cryptol.Parser.NoPat.RemovePatterns [Cryptol.Parser.AST.Decl Cryptol.Parser.Name.PName]
instance GHC.Base.Functor Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Applicative Cryptol.Parser.NoPat.NoPatM
instance GHC.Base.Monad Cryptol.Parser.NoPat.NoPatM
instance Cryptol.Utils.PP.PP Cryptol.Parser.NoPat.Error
-- | 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.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.Type
-- | 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 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
-- | The internal representation of types. These are assumed to be kind
-- correct.
data Type
-- | Type constant with args
TCon :: !TCon -> ![Type] -> Type
-- | Type variable (free or bound)
TVar :: TVar -> Type
-- | This is just a type annotation, for a type that was written as a type
-- synonym. It is useful so that we can use it to report nicer errors.
-- Example: `TUser T ts t` is really just the type t that was
-- written as `T ts` by the user.
TUser :: !Name -> ![Type] -> !Type -> Type
-- | Record type
TRec :: ![(Ident, Type)] -> Type
-- | Type variables.
data TVar
-- | Unique, kind, ids of bound type variables that are in scope The
-- Doc is a description of how this type came to be.
TVFree :: !Int -> Kind -> (Set TVar) -> Doc -> TVar
TVBound :: !Int -> Kind -> TVar
-- | The type is supposed to be of kind KProp
type Prop = Type
-- | Type constants.
data TCon
TC :: TC -> TCon
PC :: PC -> TCon
TF :: TFun -> TCon
TError :: Kind -> TCErrorMessage -> TCon
-- | Predicate symbols.
data PC
-- |
-- _ == _
--
PEqual :: PC
-- |
-- _ /= _
--
PNeq :: PC
-- |
-- _ >= _
--
PGeq :: PC
-- |
-- fin _
--
PFin :: PC
-- | Has sel type field does not appear in schemas
PHas :: Selector -> PC
-- |
-- Arith _
--
PArith :: PC
-- |
-- Cmp _
--
PCmp :: PC
-- | This is useful when simplifying things in place
PAnd :: PC
-- | Ditto
PTrue :: PC
-- | 1-1 constants.
data TC
-- | Numbers
TCNum :: Integer -> TC
-- | Inf
TCInf :: TC
-- | Bit
TCBit :: TC
-- |
-- [_] _
--
TCSeq :: TC
-- |
-- _ -> _
--
TCFun :: TC
-- |
-- (_, _, _)
--
TCTuple :: Int -> TC
-- | user-defined, T
TCNewtype :: UserTC -> TC
data UserTC
UserTC :: Name -> Kind -> UserTC
data TCErrorMessage
TCErrorMessage :: !String -> TCErrorMessage
[tcErrorMessage] :: TCErrorMessage -> !String
-- | 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)]
class HasKind t
kindOf :: HasKind t => t -> Kind
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
-- | The type is "simple" (i.e., it contains no type functions).
type SType = Type
newtypeConType :: Newtype -> Schema
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsError :: Type -> Maybe TCErrorMessage
tIsNat' :: Type -> Maybe Nat'
tIsNum :: Type -> Maybe Integer
tIsInf :: Type -> Bool
tIsVar :: Type -> Maybe TVar
tIsFun :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsBit :: Type -> Bool
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
pIsTrue :: Prop -> Bool
pIsWidth :: Prop -> Maybe Type
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
newtypeTyCon :: Newtype -> TCon
-- | Make a function type.
tFun :: Type -> Type -> Type
infixr 5 `tFun`
-- | Eliminate outermost type synonyms.
tNoUser :: Type -> Type
-- | Make a malformed numeric type.
tBadNumber :: TCErrorMessage -> Type
tf1 :: TFun -> Type -> Type
tf2 :: TFun -> Type -> Type -> Type
tf3 :: TFun -> Type -> Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tWidth :: Type -> Type
tLenFromThen :: Type -> Type -> Type -> Type
tLenFromThenTo :: Type -> 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 Has constraint, used for tuple and record selection.
pHas :: Selector -> Type -> Type -> Prop
pTrue :: Prop
pAnd :: [Prop] -> Prop
pSplitAnd :: Prop -> [Prop]
pFin :: Type -> Prop
-- | Make a malformed property.
pError :: TCErrorMessage -> Prop
class FVS t
fvs :: FVS t => t -> Set TVar
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
-- | Built-in types.
data TFun
-- |
-- : Num -> Num -> Num
--
TCAdd :: TFun
-- |
-- : Num -> Num -> Num
--
TCSub :: TFun
-- |
-- : Num -> Num -> Num
--
TCMul :: TFun
-- |
-- : Num -> Num -> Num
--
TCDiv :: TFun
-- |
-- : Num -> Num -> Num
--
TCMod :: TFun
-- |
-- : Num -> Num -> Num
--
TCExp :: TFun
-- |
-- : Num -> Num
--
TCWidth :: TFun
-- |
-- : Num -> Num -> Num
--
TCMin :: TFun
-- |
-- : Num -> Num -> Num
--
TCMax :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. ]
-- :: [lengthFromThen 1 5 b][b]
TCLenFromThen :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9
-- ] :: [lengthFromThenTo 1 5 9][b]
TCLenFromThenTo :: TFun
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Newtype
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Newtype
instance GHC.Show.Show Cryptol.TypeCheck.Type.Newtype
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TySyn
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TySyn
instance GHC.Show.Show Cryptol.TypeCheck.Type.TySyn
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Schema
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Schema
instance GHC.Show.Show Cryptol.TypeCheck.Type.Schema
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Schema
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Type
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Type
instance GHC.Show.Show Cryptol.TypeCheck.Type.Type
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TCon
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TCon
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TCon
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TCon
instance GHC.Show.Show Cryptol.TypeCheck.Type.TCon
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TCErrorMessage
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TCErrorMessage
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TCErrorMessage
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TCErrorMessage
instance GHC.Show.Show Cryptol.TypeCheck.Type.TCErrorMessage
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TC
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TC
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TC
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TC
instance GHC.Show.Show Cryptol.TypeCheck.Type.TC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.UserTC
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.UserTC
instance GHC.Show.Show Cryptol.TypeCheck.Type.UserTC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.PC
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.PC
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.PC
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.PC
instance GHC.Show.Show Cryptol.TypeCheck.Type.PC
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TVar
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TVar
instance GHC.Show.Show Cryptol.TypeCheck.Type.TVar
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.TParam
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.TParam
instance GHC.Show.Show Cryptol.TypeCheck.Type.TParam
instance Control.DeepSeq.NFData Cryptol.TypeCheck.Type.Kind
instance GHC.Generics.Generic Cryptol.TypeCheck.Type.Kind
instance GHC.Show.Show Cryptol.TypeCheck.Type.Kind
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.Kind
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Kind
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.TVar
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.TCon
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.UserTC
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.TC
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.PC
instance Cryptol.TypeCheck.Type.HasKind Cryptol.Prims.Syntax.TFun
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.TySyn
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.Newtype
instance Cryptol.TypeCheck.Type.HasKind Cryptol.TypeCheck.Type.TParam
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.Type
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.Type
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TParam
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TParam
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.UserTC
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.UserTC
instance GHC.Classes.Eq Cryptol.TypeCheck.Type.TVar
instance GHC.Classes.Ord Cryptol.TypeCheck.Type.TVar
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS (GHC.Base.Maybe a)
instance Cryptol.TypeCheck.Type.FVS a => Cryptol.TypeCheck.Type.FVS [a]
instance (Cryptol.TypeCheck.Type.FVS a, Cryptol.TypeCheck.Type.FVS b) => Cryptol.TypeCheck.Type.FVS (a, b)
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.Type.Schema
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TParam
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TParam)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Schema
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Schema)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TySyn
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TySyn)
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.Type)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Kind
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Type.TVar)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TVar
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.Type
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TCon
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TCErrorMessage
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.PC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.TC
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Type.UserTC
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]
data Expr
-- | List value (with type of elements)
EList :: [Expr] -> Type -> Expr
-- | Tuple value
ETuple :: [Expr] -> Expr
-- | Record value
ERec :: [(Ident, Expr)] -> Expr
-- | Elimination for tuplerecordlist
ESel :: Expr -> Selector -> Expr
-- | If-then-else
EIf :: Expr -> Expr -> Expr -> Expr
-- | List comprehensions The types cache the length of the sequence and its
-- element type.
EComp :: Type -> Type -> Expr -> [[Match]] -> Expr
-- | Use of a bound variable
EVar :: Name -> Expr
-- | Function Value
ETAbs :: TParam -> Expr -> Expr
-- | Type application
ETApp :: Expr -> Type -> Expr
-- | Function application
EApp :: Expr -> Expr -> Expr
-- | Function value
EAbs :: Name -> Type -> Expr -> Expr
-- | Proof abstraction. Because we don't keep proofs around we don't need
-- to name the assumption, but we still need to record the assumption.
-- The assumption is the Type term, which should be of kind
-- KProp.
EProofAbs :: Prop -> Expr -> Expr
-- | If `e : p => t`, then `EProofApp e : t`, as long as we can prove
-- p.
--
-- We don't record the actual proofs, as they are not used for anything.
-- It may be nice to keep them around for sanity checking.
EProofApp :: Expr -> Expr
EWhere :: Expr -> [DeclGroup] -> Expr
data Match
-- | Type arguments are the length and element type of the sequence
-- expression
From :: Name -> Type -> 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
-- | Construct a primitive, given a map to the unique names of the Cryptol
-- module.
ePrim :: PrimMap -> Ident -> Expr
-- | Make an expression that is error pre-applied to a type and a
-- message.
eError :: PrimMap -> Type -> String -> Expr
eString :: PrimMap -> String -> Expr
eChar :: PrimMap -> Char -> Expr
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitAbs :: Expr -> Maybe ((Name, Type), Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
data Name
-- | Built-in types.
data TFun
-- |
-- : Num -> Num -> Num
--
TCAdd :: TFun
-- |
-- : Num -> Num -> Num
--
TCSub :: TFun
-- |
-- : Num -> Num -> Num
--
TCMul :: TFun
-- |
-- : Num -> Num -> Num
--
TCDiv :: TFun
-- |
-- : Num -> Num -> Num
--
TCMod :: TFun
-- |
-- : Num -> Num -> Num
--
TCExp :: TFun
-- |
-- : Num -> Num
--
TCWidth :: TFun
-- |
-- : Num -> Num -> Num
--
TCMin :: TFun
-- |
-- : Num -> Num -> Num
--
TCMax :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. ]
-- :: [lengthFromThen 1 5 b][b]
TCLenFromThen :: TFun
-- | : Num -> Num -> Num -> Num Example: [ 1, 5 .. 9
-- ] :: [lengthFromThenTo 1 5 9][b]
TCLenFromThenTo :: TFun
-- | Selectors are used for projecting from various components. Each
-- selector has an option spec to specify the shape of the thing that is
-- being selected. Currently, there is no surface syntax for list
-- selectors, but they are used during the desugaring of patterns.
data Selector
-- | Zero-based tuple selection. Optionally specifies the shape of the
-- tuple (one-based).
TupleSel :: Int -> (Maybe Int) -> Selector
-- | Record selection. Optionally specifies the shape of the record.
RecordSel :: Ident -> (Maybe [Ident]) -> Selector
-- | List selection. Optionally specifies the length of the list.
ListSel :: Int -> (Maybe Int) -> Selector
-- | An import declaration.
data Import
Import :: !ModName -> Maybe ModName -> Maybe ImportSpec -> Import
[iModule] :: Import -> !ModName
[iAs] :: Import -> Maybe ModName
[iSpec] :: Import -> Maybe ImportSpec
-- | The list of names following an import.
--
-- INVARIANT: All of the Name entries in the list are expected
-- to be unqualified names; the QName or NewName
-- constructors should not be present.
data ImportSpec
Hiding :: [Ident] -> ImportSpec
Only :: [Ident] -> ImportSpec
-- | Export information for a declaration.
data ExportType
Public :: ExportType
Private :: ExportType
data ExportSpec name
ExportSpec :: Set name -> Set name -> ExportSpec name
[eTypes] :: ExportSpec name -> Set name
[eBinds] :: ExportSpec name -> Set name
-- | Check to see if a binding is exported.
isExportedBind :: Ord name => name -> ExportSpec name -> Bool
-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
data Pragma
PragmaNote :: String -> Pragma
PragmaProperty :: Pragma
data Fixity
Fixity :: !Assoc -> !Int -> Fixity
[fAssoc] :: Fixity -> !Assoc
[fLevel] :: Fixity -> !Int
-- | A mapping from an identifier defined in some module to its real name.
data PrimMap
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
[primDecls] :: PrimMap -> Map Ident Name
[primTypes] :: PrimMap -> Map Ident Name
data TCErrorMessage
TCErrorMessage :: !String -> TCErrorMessage
[tcErrorMessage] :: TCErrorMessage -> !String
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Module
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Module
instance GHC.Show.Show Cryptol.TypeCheck.AST.Module
instance Control.DeepSeq.NFData Cryptol.TypeCheck.AST.Match
instance GHC.Generics.Generic Cryptol.TypeCheck.AST.Match
instance GHC.Show.Show Cryptol.TypeCheck.AST.Match
instance 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 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)
-- | 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 0.
zero :: Expr
-- | The constant 1.
one :: Expr
-- | The constant 2.
two :: Expr
-- | The constant infinity.
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
-- Nothing 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 a, GHC.Classes.Eq p) => 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
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 max
-- inf (0 - 1), which one might think would simplify to
-- inf.
cryDefined :: Expr -> Prop
-- | Simplification of expressions. The result of simplifying an expression
-- e, is a new expression e', 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 Nothing 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
-- | 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 Nothing 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
-- Nothing if nothing was affected. Otherwise returns Just,
-- 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 _a =
-- e.
--
-- There should be no bindings that mention NL term names in the
-- definitions of the substition (i.e, things like x = _a 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
-- | 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 True when the intervals definitely overlap, and
-- False 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 Nothing.
iIntersect :: Interval -> Interval -> Maybe Interval
-- | Any value
iAny :: Interval
-- | Any finite value
iAnyFin :: Interval
-- | Exactly this value
iConst :: Nat' -> Interval
iAdd :: Interval -> Interval -> Interval
iMul :: Interval -> Interval -> Interval
iExp :: Interval -> Interval -> Interval
iMin :: Interval -> Interval -> Interval
iMax :: Interval -> Interval -> Interval
iSub :: Interval -> Interval -> Interval
iDiv :: Interval -> Interval -> Interval
iMod :: Interval -> Interval -> Interval
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
-- | 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:
--
--
-- - x = A variable x must equal constant
-- A
-- - x = y variable x must equal variable
-- y
-- - x = A * y + B (coming soon) variable x is a
-- linear function of y, A and B are natural
-- numbers.
--
--
-- 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 x * y = z, and we can figure out that x
-- must be 5, then we end up with a linear constraint 5 * y = z.
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.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.Type.Type
instance GHC.Show.Show a => GHC.Show.Show (Cryptol.TypeCheck.TypeMap.TypeMap a)
-- | This module implements a transformation, which tries to avoid
-- exponential slow down in some cases. What's the problem? Consider the
-- following (common) patterns:
--
-- fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]
--
-- The type of fibs is:
--
-- {a} (a >= 1, fin a) => [inf][a]
--
-- Here a is the number of bits to be used in the values
-- computed by fibs. When we evaluate fibs, a
-- becomes a parameter to fibs, which works except that now
-- fibs is a function, and we don't get any of the memoization
-- we might expect! What looked like an efficient implementation has all
-- of a sudden become exponential!
--
-- Note that this is only a problem for polymorphic values: if
-- fibs was already a function, it would not be that surprising
-- that it does not get cached.
--
-- So, to avoid this, we try to spot recursive polymorphic values, where
-- the recursive occurrences have the exact same type parameters as the
-- definition. For example, this is the case in fibs: each
-- recursive call to fibs is instantiated with exactly the same
-- type parameter (i.e., a). The rewrite we do is as follows:
--
-- fibs : {a} (a >= 1, fin a) => [inf][a] fibs = {a} (a >= 1,
-- fin a) -> fibs' where fibs' : [inf][a] fibs' = [0,1] # [ x + y | x
-- <- fibs', y <- drop`{1} fibs' ]
--
-- After the rewrite, the recursion is monomorphic (i.e., we are always
-- using the same type). As a result, fibs' is an ordinary
-- recursive value, where we get the benefit of caching.
--
-- The rewrite is a bit more complex, when there are multiple mutually
-- recursive functions. Here is an example:
--
-- zig : {a} (a >= 2, fin a) => [inf][a] zig = [1] # zag
--
-- zag : {a} (a >= 2, fin a) => [inf][a] zag = [2] # zig
--
-- This gets rewritten to:
--
-- newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a]) newName =
-- {a} (a >= 2, fin a) -> (zig', zag') where zig' : [inf][a] zig' =
-- [1] # zag'
--
-- zag' : [inf][a] zag' = [2] # zig'
--
-- zig : {a} (a >= 2, fin a) => [inf][a] zig = {a} (a >= 2, fin
-- a) -> (newName a <> <> ).1
--
-- zag : {a} (a >= 2, fin a) => [inf][a] zag = {a} (a >= 2, fin
-- a) -> (newName a <> <> ).2
--
-- NOTE: We are assuming that no capture would occur with binders. For
-- values, this is because we replaces things with freshly chosen
-- variables. For types, this should be because there should be no
-- shadowing in the types. XXX: Make sure that this really is the case
-- for types!!
module Cryptol.Transform.MonoValues
-- | Note that this assumes that this pass will be run only once for each
-- module, otherwise we will get name collisions.
rewModule :: Supply -> Module -> (Module, Supply)
instance Cryptol.TypeCheck.TypeMap.TrieMap Cryptol.Transform.MonoValues.RewMap' (Cryptol.ModuleSystem.Name.Name, [Cryptol.TypeCheck.Type.Type], GHC.Types.Int)
module Cryptol.TypeCheck.Solver.Types
type Ctxt = Map TVar Interval
data Solved
-- | Solved, assuming the sub-goals.
SolvedIf :: [Prop] -> Solved
-- | We could not solve the goal.
Unsolved :: Solved
-- | The goal can never be solved.
Unsolvable :: TCErrorMessage -> Solved
elseTry :: Solved -> Solved -> Solved
solveOpts :: [Solved] -> Solved
matchThen :: Maybe a -> (a -> Solved) -> Solved
guarded :: Bool -> Solved -> Solved
instance GHC.Show.Show Cryptol.TypeCheck.Solver.Types.Solved
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Solver.Types.Solved
-- | Solving class constraints.
module Cryptol.TypeCheck.Solver.Class
-- | Solve class constraints. If not, then we return Nothing. If
-- solved, ther we return Just a list of sub-goals.
classStep :: Prop -> Solved
-- | Solve an Arith constraint by instance, if possible.
solveArithInst :: Type -> Solved
-- | Solve Cmp constraints.
solveCmpInst :: Type -> 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 fin constraints.
module Cryptol.TypeCheck.Solver.Numeric.Fin
cryIsFin :: Map TVar Interval -> Prop -> Solved
cryIsFinType :: Map TVar Interval -> Type -> Solved
module Cryptol.TypeCheck.TypePat
aInf :: Pat Type ()
aNat :: Pat Type Integer
aNat' :: Pat Type Nat'
anAdd :: Pat Type (Type, Type)
(|-|) :: Pat Type (Type, Type)
aMul :: Pat Type (Type, Type)
(|^|) :: Pat Type (Type, Type)
(|/|) :: Pat Type (Type, Type)
(|%|) :: Pat Type (Type, Type)
aMin :: Pat Type (Type, Type)
aMax :: Pat Type (Type, Type)
aWidth :: Pat Type Type
aLenFromThen :: Pat Type (Type, Type, Type)
aLenFromThenTo :: Pat Type (Type, Type, Type)
aTVar :: Pat Type TVar
aBit :: Pat Type ()
aSeq :: Pat Type (Type, Type)
aWord :: Pat Type Type
aChar :: Pat Type ()
aTuple :: Pat Type [Type]
(|->|) :: Pat Type (Type, Type)
aFin :: Pat Prop Type
(|=|) :: Pat Prop (Type, Type)
(|/=|) :: Pat Prop (Type, Type)
(|>=|) :: Pat Prop (Type, Type)
aCmp :: Pat Prop Type
aArith :: Pat Prop Type
aAnd :: Pat Prop (Prop, Prop)
aTrue :: Pat Prop ()
anError :: Kind -> Pat Type TCErrorMessage
module Cryptol.TypeCheck.SimpType
tRebuild' :: Bool -> Type -> Type
tRebuild :: Type -> Type
tAdd :: Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tMax :: Type -> Type -> Type
tWidth :: Type -> Type
tLenFromThen :: Type -> Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat')
op1 :: (a -> b) -> [a] -> b
op2 :: (a -> a -> b) -> [a] -> b
op3 :: (a -> a -> a -> b) -> [a] -> b
-- | Common checks: check for error, or simple full evaluation.
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
module Cryptol.TypeCheck.Solver.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
module Cryptol.TypeCheck.Solver.Utils
-- | All ways to split a type in the form: `a + t1`, where a is a
-- variable.
splitVarSummands :: Type -> [(TVar, Type)]
-- | Check if we can express a type in the form: `a + t1`.
splitVarSummand :: TVar -> Type -> Maybe Type
-- | Check if we can express a type in the form: `k + t1`, where k
-- is a constant > 0. This assumes that the type has been simplified
-- already, so that constants are floated to the left.
splitConstSummand :: Type -> Maybe (Integer, Type)
-- | Check if we can express a type in the form: `k * t1`, where k
-- is a constant > 1 This assumes that the type has been simplified
-- already, so that constants are floated to the left.
splitConstFactor :: Type -> Maybe (Integer, Type)
module Cryptol.TypeCheck.Solver.Numeric
cryIsEqual :: Ctxt -> Type -> Type -> Solved
cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
cryIsGeq :: Ctxt -> Type -> Type -> Solved
module Cryptol.TypeCheck.SimpleSolver
simplify :: Ctxt -> Prop -> Prop
simplifyStep :: Ctxt -> Prop -> Solved
module Cryptol.TypeCheck.Subst
data Subst
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
class FVS t
fvs :: FVS t => t -> Set TVar
-- | Apply a substitution. Returns Nothing if nothing changed.
apSubstMaybe :: Subst -> Type -> Maybe Type
class TVars t
apSubst :: TVars t => Subst -> t -> t
-- | Apply the substitution to the keys of a type map.
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
substBinds :: Subst -> Set TVar
applySubstToVar :: Subst -> TVar -> Maybe Type
substToList :: Subst -> [(TVar, Type)]
instance GHC.Show.Show Cryptol.TypeCheck.Subst.Subst
instance Cryptol.Utils.PP.PP (Cryptol.TypeCheck.PP.WithNames Cryptol.TypeCheck.Subst.Subst)
instance Cryptol.Utils.PP.PP Cryptol.TypeCheck.Subst.Subst
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.Type.Type
instance (GHC.Base.Functor m, Cryptol.TypeCheck.Subst.TVars a) => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.List m a)
instance Cryptol.TypeCheck.Subst.TVars a => Cryptol.TypeCheck.Subst.TVars (Cryptol.TypeCheck.TypeMap.TypeMap a)
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.Type.Schema
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Expr
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Match
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclGroup
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Decl
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.DeclDef
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.AST.Module
-- | 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 :: (Set 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 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 _ -> _)
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.
UnsolvedGoals :: Bool -> [Goal] -> Error
-- | A constraint (with context) that we could not solve
UnsolvedDelayedCt :: DelayedCt -> Error
-- | Type wild cards are not allowed in this context (e.g., definitions of
-- type synonyms).
UnexpectedTypeWildCard :: Error
-- | Unification variable depends on quantified variables that are not in
-- scope.
TypeVariableEscaped :: Type -> [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 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 GHC.Classes.Eq Cryptol.TypeCheck.InferTypes.Goal
instance GHC.Classes.Ord Cryptol.TypeCheck.InferTypes.Goal
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.Type.FVS Cryptol.TypeCheck.InferTypes.Warning
instance Cryptol.TypeCheck.Subst.TVars Cryptol.TypeCheck.InferTypes.Error
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.Error
instance Cryptol.TypeCheck.Type.FVS Cryptol.TypeCheck.InferTypes.Goal
instance Cryptol.TypeCheck.Type.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)
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.Type.Type
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.Schema
instance Cryptol.TypeCheck.Sanity.Same Cryptol.TypeCheck.Type.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.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 Nothing if the currently asserted constraints are known
-- to be unsatisfiable.
--
-- Returns `Just (su, sub-goals)` is the current set is satisfiable. *
-- The su 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))
-- | dpSimpProp and dpSimpExprProp should be logically
-- equivalent, to each other, and to whatever a represents
-- (usually a is a Goal).
data DefinedProp a
DefinedProp :: a -> SimpProp -> Prop -> DefinedProp a
-- | Optional data to associate with prop. Often, the original Goal
-- 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]
loadFile :: Solver -> FilePath -> IO ()
rawSolver :: Solver -> Solver
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.Type.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.Type.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
-- | Look for opportunity to solve goals by instantiating variables.
module Cryptol.TypeCheck.Solver.Improve
-- | Improvements from a bunch of propositions. Invariant: the substitions
-- should be already applied to the new sub-goals, if any.
improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst, [Prop])
-- | Improvements from a proposition. Invariant: the substitions should be
-- already applied to the new sub-goals, if any.
improveProp :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
-- | Improvements from euqality constraints. Invariant: the substitions
-- should be already applied to the new sub-goals, if any.
improveEq :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
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.Unify
-- | The most general unifier is a substitution and a set of constraints on
-- bound variables.
type MGU = (Subst, [Prop])
data Result a
OK :: a -> Result a
Error :: UnificationError -> Result a
data UnificationError
UniTypeMismatch :: Type -> Type -> UnificationError
UniKindMismatch :: Kind -> Kind -> UnificationError
UniTypeLenMismatch :: Int -> Int -> UnificationError
UniRecursive :: TVar -> Type -> UnificationError
UniNonPolyDepends :: TVar -> [TVar] -> UnificationError
UniNonPoly :: TVar -> Type -> UnificationError
uniError :: UnificationError -> Result a
emptyMGU :: MGU
mgu :: Type -> Type -> Result MGU
mguMany :: [Type] -> [Type] -> Result MGU
bindVar :: TVar -> Type -> Result MGU
instance GHC.Base.Functor Cryptol.TypeCheck.Unify.Result
instance GHC.Base.Applicative Cryptol.TypeCheck.Unify.Result
instance GHC.Base.Monad Cryptol.TypeCheck.Unify.Result
module Cryptol.TypeCheck.Monad
-- | Information needed for type inference.
data InferInput
InferInput :: Range -> Map Name Schema -> Map Name TySyn -> Map Name Newtype -> NameSeeds -> Bool -> SolverConfig -> [FilePath] -> !PrimMap -> !Supply -> InferInput
-- | Location of program source
[inpRange] :: InferInput -> Range
-- | Variables that are in scope
[inpVars] :: InferInput -> Map Name Schema
-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map Name TySyn
-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map Name Newtype
-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds
-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool
-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig
-- | Where to look for Cryptol theory file.
[inpSearchPath] :: InferInput -> [FilePath]
-- | The mapping from Ident to Name, 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
bumpCounter :: InferM ()
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 -> !(IORef Int) -> RO
-- | Source code being analysed
[iRange] :: RO -> Range
-- | Type of variable that are in scope
[iVars] :: RO -> Map Name VarType
-- | Type variable that are in scope
[iTVars] :: RO -> [TParam]
-- | Type synonyms that are in scope
[iTSyns] :: RO -> Map Name (DefLoc, TySyn)
-- | Newtype declarations in scope
--
-- NOTE: type synonyms take precedence over newtype. The reason is that
-- we can define local type synonyms, but not local newtypes. So, either
-- a type-synonym shadows a newtype, or it was declared at the top-level,
-- but then there can't be a newtype with the same name (this should be
-- caught by the renamer).
[iNewtypes] :: RO -> Map Name (DefLoc, Newtype)
-- | NOTE: This field is lazy in an important way! It is the final version
-- of iSolvedHas in RW, and the two are tied together
-- through recursion. The field is here so that we can look thing up
-- before they are defined, which is OK because we don't need to know the
-- results until everything is done.
[iSolvedHasLazy] :: RO -> Map Int (Expr -> Expr)
-- | When this flag is set to true, bindings that lack signatures in
-- where-blocks will never be generalized. Bindings with type signatures,
-- and all bindings at top level are unaffected.
[iMonoBinds] :: RO -> Bool
[iSolver] :: RO -> Solver
[iPrimNames] :: RO -> !PrimMap
[iSolveCounter] :: RO -> !(IORef Int)
-- | 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 Int 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])
simpGoal :: Goal -> InferM [Goal]
simpGoals :: [Goal] -> InferM [Goal]
-- | Record a constraint that when we select from the first type, we should
-- get a value of the second type. The returned function should be used
-- to wrap the expression from which we are selecting (i.e., the record
-- or tuple). Plese note that the resulting expression should not be
-- forced before the constraint is solved.
newHasGoal :: Selector -> Type -> Type -> InferM (Expr -> Expr)
-- | Add a previously generate has constrained
addHasGoal :: HasGoal -> InferM ()
-- | Get the Has constraints. Each of this should either be
-- solved, or added back using addHasGoal.
getHasGoals :: InferM [HasGoal]
-- | Specify the solution (`Expr -> Expr`) for the given constraint
-- (Int).
solveHasGoal :: Int -> (Expr -> Expr) -> InferM ()
newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
-- | Generate a new name for a goal.
newGoalName :: InferM Int
-- | Generate a new free type variable.
newTVar :: Doc -> Kind -> InferM TVar
-- | Generate a new free type variable that depends on these additional
-- type parameters.
newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar
-- | Generate a new free type variable.
newTParam :: Maybe 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 Nothing 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 -> [(ConstraintSource, [Prop])] -> KRW
-- | kinds of (known) vars.
[typeParams] :: KRW -> Map Name Kind
[kCtrs] :: KRW -> [(ConstraintSource, [Prop])]
-- | 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, [(ConstraintSource, [Prop])])
-- | 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. NOTE: We do
-- not simplify these, because we end up with bottom. See hs XXX:
-- Perhaps we can avoid the recursion?
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 (Bool, Bool)
module Cryptol.TypeCheck.Solver.SMT
-- | Returns goals that were not proved
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
-- | Check if the given goals are known to be unsolvable.
checkUnsolvable :: Solver -> [Goal] -> IO Bool
instance Cryptol.TypeCheck.Solver.SMT.Mk ()
instance Cryptol.TypeCheck.Solver.SMT.Mk GHC.Integer.Type.Integer
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.TVar
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.Type
instance Cryptol.TypeCheck.Solver.SMT.Mk Cryptol.TypeCheck.Type.TCErrorMessage
instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type)
instance Cryptol.TypeCheck.Solver.SMT.Mk (Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type, Cryptol.TypeCheck.Type.Type)
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], Maybe 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))
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 NoPat 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 :: Type -> Type -> InferM ()
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)
-- | inferBinds isTopLevel isRec binds performs inference for a
-- strongly-connected component of Binds. If isTopLevel
-- is true, any bindings without type signatures will be generalized. If
-- it is false, and the mono-binds flag is enabled, no bindings without
-- type signatures will be generalized, but bindings with signatures will
-- be unaffected.
inferBinds :: Bool -> Bool -> [Bind 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 exprMap 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))
-- | 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 -> [FilePath] -> !PrimMap -> !Supply -> InferInput
-- | Location of program source
[inpRange] :: InferInput -> Range
-- | Variables that are in scope
[inpVars] :: InferInput -> Map Name Schema
-- | Type synonyms that are in scope
[inpTSyns] :: InferInput -> Map Name TySyn
-- | Newtypes in scope
[inpNewtypes] :: InferInput -> Map Name Newtype
-- | Private state of type-checker
[inpNameSeeds] :: InferInput -> NameSeeds
-- | Should local bindings without signatures be monomorphized?
[inpMonoBinds] :: InferInput -> Bool
-- | Options for the constraint solver
[inpSolverConfig] :: InferInput -> SolverConfig
-- | Where to look for Cryptol theory file.
[inpSearchPath] :: InferInput -> [FilePath]
-- | The mapping from Ident to Name, 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 _ -> _)
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.
UnsolvedGoals :: Bool -> [Goal] -> Error
-- | A constraint (with context) that we could not solve
UnsolvedDelayedCt :: DelayedCt -> Error
-- | Type wild cards are not allowed in this context (e.g., definitions of
-- type synonyms).
UnexpectedTypeWildCard :: Error
-- | Unification variable depends on quantified variables that are not in
-- scope.
TypeVariableEscaped :: Type -> [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.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 both 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
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 Ident to Name for a given naming
-- environment.
toPrimMap :: NamingEnv -> PrimMap
-- | Generate a display format based on a naming environment.
toNameDisp :: NamingEnv -> NameDisp
-- | Produce sets of visible names for types and declarations.
--
-- NOTE: if entries in the NamingEnv would have produced a name clash,
-- they will be omitted from the resulting sets.
visibleNames :: NamingEnv -> (Set Name, Set Name)
-- | Qualify all symbols in a NamingEnv with the given prefix.
qualify :: ModName -> NamingEnv -> NamingEnv
filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv
-- | Singleton type renaming environment.
singletonT :: PName -> Name -> NamingEnv
-- | Singleton expression renaming environment.
singletonE :: PName -> Name -> NamingEnv
-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv
data InModule a
InModule :: !ModName -> a -> InModule a
-- | Generate a NamingEnv using an explicit supply.
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply)
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 NameDisp for
-- pretty-printing.
interpImport :: Import -> IfaceDecls -> NamingEnv
-- | Generate a naming environment from a declaration interface, where none
-- of the names are qualified.
unqualifiedEnv :: IfaceDecls -> NamingEnv
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))
module Cryptol.ModuleSystem.Renamer
data NamingEnv
-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
-- | Things that define exported names.
class BindsNames a
namingEnv :: BindsNames a => a -> BuildNamingEnv
data InModule a
InModule :: !ModName -> a -> InModule a
-- | Generate a NamingEnv using an explicit supply.
namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply)
-- | Throw errors for any names that overlap in a rewrite environment.
checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning])
-- | Shadow the current naming environment with some more names.
shadowNames :: BindsNames env => env -> RenameM a -> RenameM a
class Rename f
rename :: Rename f => f PName -> RenameM (f Name)
runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a -> (Either [RenamerError] (a, Supply), [RenamerWarning])
data RenameM a
data RenamerError
-- | Multiple imported symbols contain this name
MultipleSyms :: (Located PName) -> [Name] -> NameDisp -> RenamerError
-- | Expression name is not bound to any definition
UnboundExpr :: (Located PName) -> NameDisp -> RenamerError
-- | Type name is not bound to any definition
UnboundType :: (Located PName) -> NameDisp -> RenamerError
-- | An environment has produced multiple overlapping symbols
OverlappingSyms :: [Name] -> NameDisp -> RenamerError
-- | When a value is expected from the naming environment, but one or more
-- types exist instead.
ExpectedValue :: (Located PName) -> NameDisp -> RenamerError
-- | When a type is missing from the naming environment, but one or more
-- values exist with the same name.
ExpectedType :: (Located PName) -> NameDisp -> RenamerError
-- | When the fixity of two operators conflict
FixityError :: (Located Name) -> (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
DangerousFixity :: (Located Name) -> (Located 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.Eval.Monad
-- | The monad for Cryptol evaluation.
data Eval a
Ready :: !a -> Eval a
Thunk :: !(IO a) -> Eval a
-- | Execute the given evaluation action.
runEval :: Eval a -> IO a
-- | Lift an IO computation into the Eval monad.
io :: IO a -> Eval a
-- | Delay the given evaluation computation, returning a thunk which will
-- run the computation when forced. Raise a loop error if the resulting
-- thunk is forced during its own evaluation.
delay :: Maybe String -> Eval a -> Eval (Eval a)
-- | Delay the given evaluation computation, returning a thunk which will
-- run the computation when forced. Run the retry computation
-- instead if the resulting thunk is forced during its own evaluation.
delayFill :: Eval a -> Eval a -> Eval (Eval a)
-- | A computation that returns an already-evaluated value.
ready :: a -> Eval a
-- | Produce a thunk value which can be filled with its associated
-- computation after the fact. A preallocated thunk is returned, along
-- with an operation to fill the thunk with the associated computation.
-- This is used to implement recursive declaration groups.
blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
-- | Data type describing errors that can occur during evaluation.
data EvalError
-- | Out-of-bounds index
InvalidIndex :: Integer -> EvalError
-- | Non-numeric type passed to demote function
TypeCannotBeDemoted :: Type -> EvalError
-- | Division or modulus by 0
DivideByZero :: EvalError
-- | Bitvector too large
WordTooWide :: Integer -> EvalError
-- | Call to the Cryptol error primitive
UserError :: String -> EvalError
-- | Detectable nontermination
LoopError :: String -> EvalError
-- | Panic from an Eval context.
evalPanic :: String -> [String] -> a
-- | For things like `(inf) or `(0-1).
typeCannotBeDemoted :: Type -> a
-- | For division by 0.
divideByZero :: Eval a
-- | For when we know that a word is too wide and will exceed gmp's limits
-- (though words approaching this size will probably cause the system to
-- crash anyway due to lack of memory).
wordTooWide :: Integer -> a
-- | For the Cryptol error function.
cryUserError :: String -> Eval a
-- | For cases where we can detect tight loops.
cryLoopError :: String -> Eval a
-- | A sequencing operation has gotten an invalid index.
invalidIndex :: Integer -> Eval a
instance GHC.Show.Show Cryptol.Eval.Monad.EvalError
instance GHC.Base.Functor Cryptol.Eval.Monad.Eval
instance GHC.Base.Applicative Cryptol.Eval.Monad.Eval
instance GHC.Base.Monad Cryptol.Eval.Monad.Eval
instance Control.Monad.IO.Class.MonadIO Cryptol.Eval.Monad.Eval
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Cryptol.Eval.Monad.Eval a)
instance Control.Monad.Fix.MonadFix Cryptol.Eval.Monad.Eval
instance Cryptol.Utils.PP.PP Cryptol.Eval.Monad.EvalError
instance GHC.Exception.Exception Cryptol.Eval.Monad.EvalError
module Cryptol.Eval.Type
-- | An evaluated type of kind *. These types do not contain type
-- variables, type synonyms, or type functions.
data TValue
-- |
-- Bit
--
TVBit :: TValue
-- |
-- [n]a
--
TVSeq :: Integer -> TValue -> TValue
-- |
-- [inf]t
--
TVStream :: TValue -> TValue
-- |
-- (a, b, c )
--
TVTuple :: [TValue] -> TValue
-- |
-- { x : a, y : b, z : c }
--
TVRec :: [(Ident, TValue)] -> TValue
-- |
-- a -> b
--
TVFun :: TValue -> TValue -> TValue
-- | Convert a type value back into a regular type
tValTy :: TValue -> Type
-- | True if the evaluated value is Bit
isTBit :: TValue -> Bool
-- | Produce a sequence type value
tvSeq :: Nat' -> TValue -> TValue
-- | Coerce an extended natural into an integer, for values known to be
-- finite
finNat' :: Nat' -> Integer
type TypeEnv = Map TVar (Either Nat' TValue)
-- | Evaluation for types (kind * or #).
evalType :: TypeEnv -> Type -> Either Nat' TValue
-- | Evaluation for value types (kind *).
evalValType :: TypeEnv -> Type -> TValue
-- | Evaluation for number types (kind #).
evalNumType :: TypeEnv -> Type -> Nat'
-- | Reduce type functions, raising an exception for undefined values.
evalTF :: TFun -> [Nat'] -> Nat'
instance Control.DeepSeq.NFData Cryptol.Eval.Type.TValue
instance GHC.Generics.Generic Cryptol.Eval.Type.TValue
instance GHC.Show.Show Cryptol.Eval.Type.TValue
-- | Architecture-specific parts of the concrete evaluator go here.
module Cryptol.Eval.Arch
-- | This is the widest word we can have before gmp will fail to allocate
-- and bring down the whole program. According to
-- https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html
-- the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however
-- experiments show that it's somewhere under 2^37 at least on 64-bit Mac
-- OS X.
maxBigIntWidth :: Integer
module Cryptol.Eval.Value
-- | Concrete bitvector values: width, value Invariant: The value must be
-- within the range 0 .. 2^width-1
data BV
BV :: !Integer -> !Integer -> BV
-- | Apply an integer function to the values of bitvectors. This function
-- assumes both bitvectors are the same width.
binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
-- | Apply an integer function to the values of a bitvector. This function
-- assumes the function will not require masking.
unaryBV :: (Integer -> Integer) -> BV -> BV
bvVal :: BV -> Integer
-- | Smart constructor for BVs that checks for the width limit
mkBv :: Integer -> Integer -> BV
-- | A sequence map represents a mapping from nonnegative integer indices
-- to values. These are used to represent both finite and infinite
-- sequences.
data SeqMap b w
IndexSeqMap :: !(Integer -> Eval (GenValue b w)) -> SeqMap b w
UpdateSeqMap :: !(Map Integer (Eval (GenValue b w))) -> !(Integer -> Eval (GenValue b w)) -> SeqMap b w
lookupSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w)
type SeqValMap = SeqMap Bool BV
-- | Generate a finite sequence map from a list of values
finiteSeqMap :: [Eval (GenValue b w)] -> SeqMap b w
-- | Generate an infinite sequence map from a stream of values
infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
-- | Create a finite list of length n of the values from [0..n-1]
-- in the given the sequence emap.
enumerateSeqMap :: (Integral n) => n -> SeqMap b w -> [Eval (GenValue b w)]
-- | Create an infinite stream of all the values in a sequence map
streamSeqMap :: SeqMap b w -> [Eval (GenValue b w)]
-- | Reverse the order of a finite sequence map
reverseSeqMap :: Integer -> SeqMap b w -> SeqMap b w
updateSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w) -> SeqMap b w
-- | Given a number n and a sequence map, return two new sequence
-- maps: the first containing the values from `[0..n-1]` and the next
-- containing the values from n onward.
splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w)
-- | Given a sequence map, return a new sequence map that is memoized using
-- a finite map memo table.
memoMap :: SeqMap b w -> Eval (SeqMap b w)
-- | Apply the given evaluation function pointwise to the two given
-- sequence maps.
zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> SeqMap b w -> Eval (SeqMap b w)
-- | Apply the given function to each value in the given sequence map
mapSeqMap :: (GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> Eval (SeqMap b w)
-- | For efficency reasons, we handle finite sequences of bits as special
-- cases in the evaluator. In cases where we know it is safe to do so, we
-- prefer to used a "packed word" representation of bit sequences. This
-- allows us to rely directly on Integer types (in the concrete
-- evalautor) and SBV's Word types (in the symbolic simulator).
--
-- However, if we cannot be sure all the bits of the sequence will
-- eventually be forced, we must instead rely on an explicit sequence of
-- bits representation.
data WordValue b w
-- | Packed word representation for bit sequences.
WordVal :: !w -> WordValue b w
-- | Sequence of thunks representing bits.
BitsVal :: !(Seq (Eval b)) -> WordValue b w
-- | Force a word value into packed word form
asWordVal :: BitWord b w => WordValue b w -> Eval w
-- | Force a word value into a sequence of bits
asBitsVal :: BitWord b w => WordValue b w -> Seq (Eval b)
-- | Select an individual bit from a word value
indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b
-- | Generic value type, parameterized by bit and word types.
--
-- NOTE: we maintain an important invariant regarding sequence types.
-- VSeq must never be used for finite sequences of bits. Always
-- use the VWord constructor instead! Infinite sequences of bits
-- are handled by the VStream constructor, just as for other
-- types.
data GenValue b w
-- |
-- { .. }
--
VRecord :: ![(Ident, Eval (GenValue b w))] -> GenValue b w
-- |
-- ( .. )
--
VTuple :: ![Eval (GenValue b w)] -> GenValue b w
-- |
-- Bit
--
VBit :: !b -> GenValue b w
-- | [n]a Invariant: VSeq is never a sequence of bits
VSeq :: !Integer -> !(SeqMap b w) -> GenValue b w
-- |
-- [n]Bit
--
VWord :: !Integer -> !(Eval (WordValue b w)) -> GenValue b w
-- |
-- [inf]a
--
VStream :: !(SeqMap b w) -> GenValue b w
-- | functions
VFun :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
-- | polymorphic values (kind *)
VPoly :: (TValue -> Eval (GenValue b w)) -> GenValue b w
-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Eval (GenValue b w)) -> GenValue b w
-- | Force the evaluation of a word value
forceWordValue :: WordValue b w -> Eval ()
-- | Force the evaluation of a value
forceValue :: GenValue b w -> Eval ()
type Value = GenValue Bool BV
data PPOpts
PPOpts :: Bool -> Int -> Int -> PPOpts
[useAscii] :: PPOpts -> Bool
[useBase] :: PPOpts -> Int
[useInfLength] :: PPOpts -> Int
defaultPPOpts :: PPOpts
atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
ppValue :: forall b w. BitWord b w => PPOpts -> GenValue b w -> Eval Doc
asciiMode :: PPOpts -> Integer -> Bool
integerToChar :: Integer -> Char
ppBV :: PPOpts -> BV -> Doc
-- | This type class defines a collection of operations on bits and words
-- that are necessary to define generic evaluator primitives that operate
-- on both concrete and symbolic values uniformly.
class BitWord b w | b -> w, w -> b
-- | Pretty-print an individual bit
ppBit :: BitWord b w => b -> Doc
-- | Pretty-print a word value
ppWord :: BitWord b w => PPOpts -> w -> Doc
-- | Attempt to render a word value as an ASCII character. Return
-- Nothing if the character value is unknown (e.g., for symbolic
-- values).
wordAsChar :: BitWord b w => w -> Maybe Char
-- | The number of bits in a word value.
wordLen :: BitWord b w => w -> Integer
-- | Construct a literal bit value from a boolean.
bitLit :: BitWord b w => Bool -> b
-- | Construct a literal word value given a bit width and a value.
wordLit :: BitWord b w => Integer -> Integer -> w
-- | Construct a word value from a finite sequence of bits. NOTE: this
-- assumes that the sequence of bits is big-endian and finite, so the
-- first element of the list will be the most significant bit.
packWord :: BitWord b w => [b] -> w
-- | Deconstruct a packed word value in to a finite sequence of bits. NOTE:
-- this produces a list of bits that represent a big-endian word, so the
-- most significant bit is the first element of the list.
unpackWord :: BitWord b w => w -> [b]
-- | Concatenate the two given word values. NOTE: the first argument
-- represents the more-significant bits
joinWord :: BitWord b w => w -> w -> w
-- | Take the most-significant bits, and return those bits and the
-- remainder. The first element of the pair is the most significant bits.
-- The two integer sizes must sum to the length of the given word value.
splitWord :: BitWord b w => Integer -> Integer -> w -> (w, w)
-- | Extract a subsequence of bits from a packed word value. The first
-- integer argument is the number of bits in the resulting word. The
-- second integer argument is the number of less-significant digits to
-- discard. Stated another way, the operation `extractWord n i w` is
-- equivelant to first shifting w right by i bits, and
-- then truncating to n bits.
extractWord :: BitWord b w => Integer -> Integer -> w -> w
-- | 2's complement addition of packed words. The arguments must have equal
-- bit width, and the result is of the same width. Overflow is silently
-- discarded.
wordPlus :: BitWord b w => w -> w -> w
-- | 2's complement subtraction of packed words. The arguments must have
-- equal bit width, and the result is of the same width. Overflow is
-- silently discarded.
wordMinus :: BitWord b w => w -> w -> w
-- | 2's complement multiplication of packed words. The arguments must have
-- equal bit width, and the result is of the same width. The high bits of
-- the multiplication are silently discarded.
wordMult :: BitWord b w => w -> w -> w
-- | This class defines additional operations necessary to define generic
-- evaluation functions.
class BitWord b w => EvalPrims b w
-- | Eval prim binds primitive declarations to the primitive values that
-- implement them.
evalPrim :: EvalPrims b w => Decl -> GenValue b w
-- | ifthenelse operation. Choose either the 'then' value or the
-- 'else' value depending on the value of the test bit.
iteValue :: EvalPrims b w => b -> Eval (GenValue b w) -> Eval (GenValue b w) -> Eval (GenValue b w)
mask :: Integer -> Integer -> Integer
-- | Create a packed word of n bits.
word :: BitWord b w => Integer -> Integer -> GenValue b w
lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
-- | Functions that assume word inputs
wlam :: BitWord b w => (w -> Eval (GenValue b w)) -> GenValue b w
-- | A type lambda that expects a Type.
tlam :: (TValue -> GenValue b w) -> GenValue b w
-- | A type lambda that expects a Type of kind #.
nlam :: (Nat' -> GenValue b w) -> GenValue b w
-- | Generate a stream.
toStream :: [GenValue b w] -> Eval (GenValue b w)
toFinSeq :: BitWord b w => Integer -> 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 :: BitWord b w => Nat' -> TValue -> [GenValue b w] -> Eval (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.
mkSeq :: Nat' -> TValue -> SeqMap b w -> GenValue b w
-- | Extract a bit value.
fromVBit :: GenValue b w -> b
bitsSeq :: BitWord b w => WordValue b w -> Integer -> Eval b
-- | Extract a sequence.
fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w)
fromStr :: Value -> Eval String
fromWordVal :: String -> GenValue b w -> Eval (WordValue b w)
-- | Extract a packed word.
fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
vWordLen :: BitWord b w => GenValue b w -> Maybe Integer
-- | If the given list of values are all fully-evaluated thunks containing
-- bits, return a packed word built from the same bits. However, if any
-- value is not a fully-evaluated bit, return Nothing.
tryFromBits :: BitWord b w => [Eval (GenValue b w)] -> Maybe w
-- | Turn a value into an integer represented by w bits.
fromWord :: String -> Value -> Eval Integer
-- | Extract a function from a value.
fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w))
-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue b w -> (TValue -> Eval (GenValue b w))
-- | Extract a polymorphic function from a value.
fromVNumPoly :: GenValue b w -> (Nat' -> Eval (GenValue b w))
-- | Extract a tuple from a value.
fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
-- | Extract a record from a value.
fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))]
-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue b w -> Eval (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 -> Eval (Maybe Expr)
instance (Control.DeepSeq.NFData w, Control.DeepSeq.NFData b) => Control.DeepSeq.NFData (Cryptol.Eval.Value.GenValue b w)
instance GHC.Generics.Generic (Cryptol.Eval.Value.GenValue b w)
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Value.WordValue b w)
instance GHC.Generics.Generic (Cryptol.Eval.Value.WordValue b w)
instance Control.DeepSeq.NFData Cryptol.Eval.Value.BV
instance GHC.Generics.Generic Cryptol.Eval.Value.BV
instance GHC.Show.Show Cryptol.Eval.Value.BV
instance Control.DeepSeq.NFData (Cryptol.Eval.Value.SeqMap b w)
instance (GHC.Show.Show b, GHC.Show.Show w) => GHC.Show.Show (Cryptol.Eval.Value.GenValue b w)
instance Cryptol.Eval.Value.BitWord GHC.Types.Bool Cryptol.Eval.Value.BV
module Cryptol.Eval.Env
data GenEvalEnv b w
EvalEnv :: !(Map Name (Eval (GenValue b w))) -> !TypeEnv -> GenEvalEnv b w
[envVars] :: GenEvalEnv b w -> !(Map Name (Eval (GenValue b w)))
[envTypes] :: GenEvalEnv b w -> !TypeEnv
ppEnv :: BitWord b w => PPOpts -> GenEvalEnv b w -> Eval Doc
-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv b w
-- | Bind a variable in the evaluation environment.
bindVar :: Name -> Eval (GenValue b w) -> GenEvalEnv b w -> Eval (GenEvalEnv b w)
-- | Bind a variable to a value in the evaluation environment, without
-- creating a thunk.
bindVarDirect :: Name -> GenValue b w -> GenEvalEnv b w -> Eval (GenEvalEnv b w)
-- | Lookup a variable in the environment.
lookupVar :: Name -> GenEvalEnv b w -> Maybe (Eval (GenValue b w))
-- | Bind a type variable of kind *.
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w -> GenEvalEnv b w
-- | Lookup a type variable.
lookupType :: TVar -> GenEvalEnv b w -> Maybe (Either Nat' TValue)
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData w) => Control.DeepSeq.NFData (Cryptol.Eval.Env.GenEvalEnv b w)
instance GHC.Generics.Generic (Cryptol.Eval.Env.GenEvalEnv b w)
instance GHC.Base.Monoid (Cryptol.Eval.Env.GenEvalEnv b w)
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
-- | True if the evaluated value is Bit
isTBit :: TValue -> Bool
-- | Produce a sequence type value
tvSeq :: Nat' -> TValue -> TValue
-- | Generic value type, parameterized by bit and word types.
--
-- NOTE: we maintain an important invariant regarding sequence types.
-- VSeq must never be used for finite sequences of bits. Always
-- use the VWord constructor instead! Infinite sequences of bits
-- are handled by the VStream constructor, just as for other
-- types.
data GenValue b w
-- |
-- { .. }
--
VRecord :: ![(Ident, Eval (GenValue b w))] -> GenValue b w
-- |
-- ( .. )
--
VTuple :: ![Eval (GenValue b w)] -> GenValue b w
-- |
-- Bit
--
VBit :: !b -> GenValue b w
-- | [n]a Invariant: VSeq is never a sequence of bits
VSeq :: !Integer -> !(SeqMap b w) -> GenValue b w
-- |
-- [n]Bit
--
VWord :: !Integer -> !(Eval (WordValue b w)) -> GenValue b w
-- |
-- [inf]a
--
VStream :: !(SeqMap b w) -> GenValue b w
-- | functions
VFun :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
-- | polymorphic values (kind *)
VPoly :: (TValue -> Eval (GenValue b w)) -> GenValue b w
-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Eval (GenValue b w)) -> GenValue b w
lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
-- | A type lambda that expects a Type.
tlam :: (TValue -> GenValue b w) -> GenValue b w
-- | Generate a stream.
toStream :: [GenValue b w] -> Eval (GenValue b w)
toFinSeq :: BitWord b w => Integer -> 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 :: BitWord b w => Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w)
-- | Extract a bit value.
fromVBit :: GenValue b w -> b
-- | Extract a function from a value.
fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w))
-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue b w -> (TValue -> Eval (GenValue b w))
-- | Extract a tuple from a value.
fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
-- | Extract a record from a value.
fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))]
-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w)
-- | Extract a sequence.
fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w)
-- | Extract a packed word.
fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
evalPanic :: String -> [String] -> a
iteSValue :: SBool -> Value -> Value -> Value
mergeValue :: Bool -> SBool -> Value -> Value -> Value
mergeWord :: Bool -> SBool -> WordValue SBool SWord -> WordValue SBool SWord -> WordValue SBool SWord
mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord -> SeqMap SBool SWord -> SeqMap SBool SWord
instance Cryptol.Eval.Value.BitWord Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord
module Cryptol.Testing.Concrete
-- | A test result is either a pass, a failure due to evaluating to
-- False, or a failure due to an exception raised during
-- evaluation
data TestResult
Pass :: TestResult
FailFalse :: [Value] -> TestResult
FailError :: EvalError -> [Value] -> TestResult
isPass :: TestResult -> Bool
-- | Apply a testable value to some arguments. Note that this function
-- assumes that the values come from a call to testableType (i.e.,
-- things are type-correct). We run in the IO monad in order to catch any
-- EvalErrors.
runOneTest :: 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 Nothing for infinite types, user-defined types,
-- polymorhic types, and, currently, function spaces. Of course, we can
-- easily compute the sizes of function spaces, but we can't easily
-- enumerate their inhabitants.
typeSize :: Type -> Maybe Integer
-- | Returns all the values in a type. Returns an empty list of values, for
-- types where typeSize returned Nothing.
typeValues :: Type -> [Value]
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
-- | 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
-- Nothing if the function returned True, or `Just
-- counterexample` if it returned False.
--
-- Please note that this function assumes that the generators match the
-- supplied value, otherwise we'll panic.
runOneTest :: RandomGen g => Value -> [Gen g] -> 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
-- [w]) The size parameter is assumed to vary between 1 and 100,
-- and we use it to generate smaller numbers first.
randomWord :: RandomGen g => Integer -> Gen g
-- | Generate a random infinite stream value.
randomStream :: RandomGen g => Gen g -> Gen g
-- | Generate a random sequence. This should be used for sequences other
-- than bits. For sequences of bits use "randomWord".
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
primTable :: Map Ident Value
-- | Make a numeric constant.
ecDemoteV :: BitWord b w => GenValue b w
divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)
-- | Create a packed word
modExp :: Integer -> BV -> BV -> Eval BV
doubleAndAdd :: Integer -> Integer -> Integer -> Integer
type Binary b w = TValue -> GenValue b w -> GenValue b w -> Eval (GenValue b w)
binary :: Binary b w -> GenValue b w
type Unary b w = TValue -> GenValue b w -> Eval (GenValue b w)
unary :: Unary 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 BV
-- | Turn a normal binop on Integers into one that can also deal with a
-- bitsize. Generate a thunk that throws a divide by 0 error when forced
-- if the second argument is 0.
liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV
type BinArith w = Integer -> w -> w -> Eval w
arithBinary :: forall b w. BitWord b w => BinArith w -> Binary b w
type UnaryArith w = Integer -> w -> Eval w
liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV
arithUnary :: forall b w. BitWord b w => UnaryArith w -> Unary b w
lg2 :: Integer -> Integer
-- | Lexicographic ordering on two values.
lexCompare :: String -> TValue -> Value -> Value -> Eval Ordering
zipLexCompare :: String -> [TValue] -> [Eval Value] -> [Eval Value] -> Eval Ordering
-- | Process two elements based on their lexicographic ordering.
cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV
withOrder :: String -> (Ordering -> TValue -> Value -> Value -> Value) -> Binary Bool BV
maxV :: Ordering -> TValue -> Value -> Value -> Value
minV :: Ordering -> TValue -> Value -> Value -> Value
funCmp :: (Ordering -> Bool) -> Value
zeroV :: forall b w. BitWord b w => TValue -> GenValue b w
joinWordVal :: BitWord b w => WordValue b w -> WordValue b w -> WordValue b w
joinWords :: forall b w. BitWord b w => Integer -> Integer -> SeqMap b w -> Eval (GenValue b w)
joinSeq :: BitWord b w => Nat' -> Integer -> TValue -> SeqMap b w -> Eval (GenValue b w)
-- | Join a sequence of sequences into a single sequence.
joinV :: BitWord b w => Nat' -> Integer -> TValue -> GenValue b w -> Eval (GenValue b w)
splitWordVal :: BitWord b w => Integer -> Integer -> WordValue b w -> (WordValue b w, WordValue b w)
splitAtV :: BitWord b w => Nat' -> Nat' -> TValue -> GenValue b w -> Eval (GenValue b w)
extractWordVal :: BitWord b w => Integer -> Integer -> WordValue b w -> WordValue b w
-- | Split implementation.
ecSplitV :: BitWord b w => GenValue b w
reverseV :: forall b w. BitWord b w => GenValue b w -> Eval (GenValue b w)
transposeV :: BitWord b w => Nat' -> Nat' -> TValue -> GenValue b w -> Eval (GenValue b w)
ccatV :: (Show b, Show w, BitWord b w) => Nat' -> Nat' -> TValue -> (GenValue b w) -> (GenValue b w) -> Eval (GenValue b w)
wordValLogicOp :: BitWord b w => (b -> b -> b) -> (w -> w -> w) -> WordValue b w -> WordValue b w -> WordValue b w
-- | Merge two values given a binop. This is used for and, or and xor.
logicBinary :: forall b w. BitWord b w => (b -> b -> b) -> (w -> w -> w) -> Binary b w
wordValUnaryOp :: BitWord b w => (b -> b) -> (w -> w) -> WordValue b w -> WordValue b w
logicUnary :: forall b w. BitWord b w => (b -> b) -> (w -> w) -> Unary b w
logicShift :: (Integer -> Integer -> Integer -> Integer) -> (Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)) -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) -> Value
shiftLW :: Integer -> Integer -> Integer -> Integer
shiftLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftRW :: Integer -> Integer -> Integer -> Integer
shiftRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateLW :: Integer -> Integer -> Integer -> Integer
rotateLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateRW :: Integer -> Integer -> Integer -> Integer
rotateRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
-- | Indexing operations that return one element.
indexPrimOne :: BitWord b w => (Maybe Integer -> TValue -> SeqMap b w -> Seq b -> Eval (GenValue b w)) -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) -> GenValue b w
indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
-- | Indexing operations that return many elements.
indexPrimMany :: BitWord b w => (Maybe Integer -> TValue -> SeqMap b w -> Seq b -> Eval (GenValue b w)) -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) -> GenValue b w
updateFront :: Nat' -> TValue -> SeqMap Bool BV -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (SeqMap Bool BV)
updateFront_bits :: Nat' -> TValue -> Seq (Eval Bool) -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (Seq (Eval Bool))
updateBack :: Nat' -> TValue -> SeqMap Bool BV -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (SeqMap Bool BV)
updateBack_bits :: Nat' -> TValue -> Seq (Eval Bool) -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (Seq (Eval Bool))
updatePrim :: BitWord b w => (Nat' -> TValue -> Seq (Eval b) -> WordValue b w -> Eval (GenValue b w) -> Eval (Seq (Eval b))) -> (Nat' -> TValue -> SeqMap b w -> WordValue b w -> Eval (GenValue b w) -> Eval (SeqMap b w)) -> GenValue b w
fromThenV :: BitWord b w => GenValue b w
fromToV :: BitWord b w => GenValue b w
fromThenToV :: BitWord b w => GenValue b w
infFromV :: BitWord b w => GenValue b w
infFromThenV :: BitWord b w => GenValue b w
-- | 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
errorV :: forall b w. BitWord b w => TValue -> String -> Eval (GenValue b w)
instance Cryptol.Eval.Value.EvalPrims GHC.Types.Bool Cryptol.Eval.Value.BV
module Cryptol.Symbolic.Prims
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
primTable :: Map Ident Value
iteWord :: SBool -> Eval (WordValue SBool SWord) -> Eval (WordValue SBool SWord) -> Eval (WordValue SBool SWord)
-- | Barrel-shifter algorithm. Takes a list of bits in big-endian order.
shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a
logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value
selectV :: forall a. (SBool -> Eval a -> Eval a -> Eval a) -> WordValue SBool SWord -> (Integer -> Eval a) -> Eval a
indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord -> SWord -> Eval Value
indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord -> SWord -> Eval Value
indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord -> Seq SBool -> Eval Value
indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord -> Seq SBool -> Eval Value
updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (SeqMap SBool SWord)
updateFrontSym_bits :: Nat' -> TValue -> Seq (Eval SBool) -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (Seq (Eval SBool))
updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (SeqMap SBool SWord)
updateBackSym_bits :: Nat' -> TValue -> Seq (Eval SBool) -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (Seq (Eval SBool))
asBitList :: [Eval SBool] -> Maybe [SBool]
asWordList :: [WordValue SBool SWord] -> Maybe [SWord]
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
sExp :: Integer -> SWord -> SWord -> Eval SWord
-- | Ceiling (log_2 x)
sLg2 :: Integer -> SWord -> Eval SWord
cmpValue :: (SBool -> SBool -> Eval a -> Eval a) -> (SWord -> SWord -> Eval a -> Eval a) -> (Value -> Value -> Eval a -> Eval a)
cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) -> (SWord -> SWord -> Eval SBool -> Eval SBool) -> SBool -> Binary SBool SWord
-- | Add two polynomials
addPoly :: [SBool] -> [SBool] -> [SBool]
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
degree :: [SBool] -> Int
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
nth :: [SBool] -> Int -> SBool
divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
instance Cryptol.Eval.Value.EvalPrims Cryptol.Symbolic.Value.SBool Cryptol.Symbolic.Value.SWord
module Cryptol.Eval
-- | Extend the given evaluation environment with all the declarations
-- contained in the given module.
moduleEnv :: EvalPrims b w => Module -> GenEvalEnv b w -> Eval (GenEvalEnv b w)
-- | Execute the given evaluation action.
runEval :: Eval a -> IO a
-- | The monad for Cryptol evaluation.
data Eval a
type EvalEnv = GenEvalEnv Bool BV
-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv b w
-- | Evaluate a Cryptol expression to a value. This evaluator is
-- parameterized by the EvalPrims class, which defines the
-- behavior of bits and words, in addition to providing implementations
-- for all the primitives.
evalExpr :: EvalPrims b w => GenEvalEnv b w -> Expr -> Eval (GenValue b w)
-- | Extend the given evaluation environment with the result of evaluating
-- the given collection of declaration groups.
evalDecls :: EvalPrims b w => [DeclGroup] -> GenEvalEnv b w -> Eval (GenEvalEnv b w)
-- | Data type describing errors that can occur during evaluation.
data EvalError
-- | Out-of-bounds index
InvalidIndex :: Integer -> EvalError
-- | Non-numeric type passed to demote function
TypeCannotBeDemoted :: Type -> EvalError
-- | Division or modulus by 0
DivideByZero :: EvalError
-- | Bitvector too large
WordTooWide :: Integer -> EvalError
-- | Call to the Cryptol error primitive
UserError :: String -> EvalError
-- | Detectable nontermination
LoopError :: String -> EvalError
-- | Force the evaluation of a value
forceValue :: GenValue b w -> Eval ()
instance GHC.Base.Monoid (Cryptol.Eval.ListEnv b w)
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 NameDisp for pretty-printing names
-- according to the imports.
--
-- XXX This could really do with some better error handling, just
-- returning mempty when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
-- | The unqualified declarations and name environment for the dynamic
-- environment.
dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
-- | Retrieve all IfaceDecls 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 m must precede
-- m in the list.
newtype LoadedModules
LoadedModules :: [LoadedModule] -> LoadedModules
[getLoadedModules] :: LoadedModules -> [LoadedModule]
data LoadedModule
LoadedModule :: ModName -> FilePath -> FilePath -> Iface -> Module -> LoadedModule
[lmName] :: LoadedModule -> ModName
-- | The file path used to load this module (may not be canonical)
[lmFilePath] :: LoadedModule -> FilePath
-- | The canonical version of the path of this module
[lmCanonicalPath] :: LoadedModule -> FilePath
[lmInterface] :: LoadedModule -> Iface
[lmModule] :: LoadedModule -> Module
isLoaded :: ModName -> LoadedModules -> Bool
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
addLoadedModule :: FilePath -> FilePath -> Module -> LoadedModules -> LoadedModules
removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
-- | Extra information we need to carry around to dynamically extend an
-- environment outside the context of a single module. Particularly
-- useful when dealing with interactive declarations as in :let
-- or it.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv
-- | Build IfaceDecls that correspond to all of the bindings in the
-- dynamic environment.
--
-- XXX: if we ever add type synonyms or newtypes at the REPL, revisit
-- this.
deIfaceDecls :: DynamicEnv -> IfaceDecls
instance 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 -> FilePath -> Module -> ModuleM ()
modifyEvalEnv :: (EvalEnv -> Eval EvalEnv) -> ModuleM ()
getEvalEnv :: ModuleM EvalEnv
getFocusedModule :: ModuleM (Maybe ModName)
setFocusedModule :: ModName -> ModuleM ()
getSearchPath :: ModuleM [FilePath]
-- | Run a ModuleM action in a context with a prepended search path.
-- Useful for temporarily looking in other places while resolving
-- imports, for example.
withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
getFocusedEnv :: ModuleM (IfaceDecls, 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)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (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:
--
--
-- import foo as foo [ [hiding] (a,b,c) ]
--
fullyQualified :: Import -> Import
-- | Find the interface referenced by an import, and generate the naming
-- environment that it describes.
importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)
-- | Load a series of interfaces, merging their public interfaces.
importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)
moduleFile :: ModName -> String -> FilePath
-- | Discover a module.
findModule :: ModName -> ModuleM FilePath
-- | Discover a file. This is distinct from findModule in that we
-- assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath
-- | 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 :let
-- or it.
data DynamicEnv
DEnv :: NamingEnv -> [DeclGroup] -> EvalEnv -> DynamicEnv
[deNames] :: DynamicEnv -> NamingEnv
[deDecls] :: DynamicEnv -> [DeclGroup]
[deEnv] :: DynamicEnv -> EvalEnv
data ModuleError
-- | Unable to find the module given, tried looking in these paths
ModuleNotFound :: ModName -> [FilePath] -> ModuleError
-- | Unable to open a file
CantFindFile :: FilePath -> ModuleError
-- | Some other IO error occurred while reading this file
OtherIOError :: FilePath -> IOException -> ModuleError
-- | Generated this parse error when parsing the file for module m
ModuleParseError :: FilePath -> ParseError -> ModuleError
-- | Recursive module group discovered
RecursiveModules :: [ImportSource] -> ModuleError
-- | Problems during the renaming phase
RenamerErrors :: ImportSource -> [RenamerError] -> ModuleError
-- | Problems during the NoPat phase
NoPatErrors :: ImportSource -> [Error] -> ModuleError
-- | Problems during the NoInclude phase
NoIncludeErrors :: ImportSource -> [IncludeError] -> ModuleError
-- | Problems during type checking
TypeCheckingFailed :: ImportSource -> [(Range, Error)] -> ModuleError
-- | Problems after type checking, eg. specialization
OtherFailure :: String -> ModuleError
-- | Module loaded by 'import' statement has the wrong module name
ModuleNameMismatch :: ModName -> (Located ModName) -> ModuleError
-- | Two modules loaded from different files have the same module name
DuplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleError
data ModuleWarning
TypeCheckWarnings :: [(Range, Warning)] -> ModuleWarning
RenamerWarnings :: [RenamerWarning] -> ModuleWarning
type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
-- | Find the file associated with a module name in the module search path.
findModule :: ModName -> ModuleCmd FilePath
-- | Load the module contained in the given file.
loadModuleByPath :: FilePath -> ModuleCmd Module
-- | Load the given parsed module.
loadModule :: FilePath -> Module 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 NameDisp for pretty-printing names
-- according to the imports.
--
-- XXX This could really do with some better error handling, just
-- returning mempty when one of the imports fails isn't really desirable.
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.Eval.Reference
-- | Value type for the reference evaluator.
data Value
-- | Bit booleans
VBit :: (Either EvalError Bool) -> Value
-- | [n]a finite or infinite lists
VList :: [Value] -> Value
-- | ( .. ) tuples
VTuple :: [Value] -> Value
-- | { .. } records
VRecord :: [(Ident, Value)] -> Value
-- | functions
VFun :: (Value -> Value) -> Value
-- | polymorphic values (kind *)
VPoly :: (TValue -> Value) -> Value
-- | polymorphic values (kind #)
VNumPoly :: (Nat' -> Value) -> Value
evaluate :: Expr -> ModuleCmd Value
ppValue :: Value -> Doc
instance GHC.Base.Monoid Cryptol.Eval.Reference.Env
module Cryptol.Transform.Specialize
-- | A Name should have an entry in the SpecCache iff it is specializable.
-- Each Name starts out with an empty TypesMap.
type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl))
-- | The specializer monad.
type SpecT m a = StateT SpecCache (ModuleT m) a
type SpecM a = SpecT IO a
runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
liftSpecT :: Monad m => ModuleT m a -> SpecT m a
getSpecCache :: Monad m => SpecT m SpecCache
setSpecCache :: Monad m => SpecCache -> SpecT m ()
modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m ()
modify :: StateM m s => (s -> s) -> m ()
-- | Add a `where` clause to the given expression containing
-- type-specialized versions of all functions called (transitively) by
-- the body of the expression.
specialize :: Expr -> ModuleCmd Expr
specializeExpr :: Expr -> SpecM Expr
specializeMatch :: Match -> SpecM Match
-- | Add the declarations to the SpecCache, run the given monadic action,
-- and then pull the specialized declarations back out of the SpecCache
-- state. Return the result along with the declarations and a table of
-- names of specialized bindings.
withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
-- | Compute the specialization of `EWhere e dgs`. A decl within
-- dgs is replicated once for each monomorphic type instance at
-- which it is used; decls not mentioned in e (even monomorphic
-- ones) are simply dropped.
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr
-- | Transform the given declaration groups into a set of monomorphic
-- declarations. All of the original declarations with monomorphic types
-- are kept; additionally the result set includes instantiated versions
-- of polymorphic decls that are referenced by the monomorphic bindings.
-- We also return a map relating generated names to the names from the
-- original declarations.
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name))
specializeConst :: Expr -> SpecM Expr
destEProofApps :: Expr -> (Expr, Int)
destETApps :: Expr -> (Expr, [Type])
destEProofAbs :: Expr -> ([Prop], Expr)
destETAbs :: Expr -> ([TParam], Expr)
-- | Freshen a name by giving it a new unique.
freshName :: Name -> [Type] -> SpecM Name
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema
-- | Reduce `length ts` outermost type abstractions and n proof
-- abstractions.
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
allDeclGroups :: ModuleEnv -> [DeclGroup]
allLoadedModules :: ModuleEnv -> [LoadedModule]
allPublicNames :: ModuleEnv -> [Name]
traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
module Cryptol.Symbolic
type EvalEnv = GenEvalEnv SBool SWord
proverConfigs :: [(String, SMTConfig)]
proverNames :: [String]
lookupProver :: String -> SMTConfig
type SatResult = [(Type, Expr, Value)]
data SatNum
AllSat :: SatNum
SomeSat :: Int -> SatNum
data QueryType
SatQuery :: SatNum -> QueryType
ProveQuery :: QueryType
data ProverCommand
ProverCommand :: QueryType -> String -> Bool -> !(IORef ProverStats) -> [DeclGroup] -> Maybe FilePath -> Expr -> Schema -> ProverCommand
-- | The type of query to run
[pcQueryType] :: ProverCommand -> QueryType
-- | Which prover to use (one of the strings in proverConfigs)
[pcProverName] :: ProverCommand -> String
-- | Verbosity flag passed to SBV
[pcVerbose] :: ProverCommand -> Bool
-- | Record timing information here
[pcProverStats] :: ProverCommand -> !(IORef ProverStats)
-- | Extra declarations to bring into scope for symbolic simulation
[pcExtraDecls] :: ProverCommand -> [DeclGroup]
-- | Optionally output the SMTLIB query to a file
[pcSmtFile] :: ProverCommand -> Maybe FilePath
-- | The typechecked expression to evaluate
[pcExpr] :: ProverCommand -> Expr
-- | The Schema of pcExpr
[pcSchema] :: ProverCommand -> Schema
type ProverStats = NominalDiffTime
-- | A prover result is either an error message, an empty result (eg for
-- the offline prover), a counterexample or a lazy list of satisfying
-- assignments.
data ProverResult
AllSatResult :: [SatResult] -> ProverResult
ThmResult :: [Type] -> ProverResult
EmptyResult :: ProverResult
ProverError :: String -> ProverResult
satSMTResults :: SatResult -> [SMTResult]
allSatSMTResults :: AllSatResult -> [SMTResult]
thmSMTResults :: ThmResult -> [SMTResult]
proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)
satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
parseValues :: [FinType] -> [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
instance GHC.Show.Show Cryptol.Symbolic.QueryType
instance GHC.Show.Show Cryptol.Symbolic.SatNum
module Cryptol.REPL.Monad
-- | REPL_ context with InputT handling.
newtype REPL a
REPL :: (IORef RW -> IO a) -> REPL a
[unREPL] :: REPL a -> IORef RW -> IO a
-- | Run a REPL action with a fresh environment.
runREPL :: Bool -> 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 #
-- that is not lexically valid in a module name.
uniqify :: Name -> REPL Name
-- | Generate a fresh name using the given index. The name will reside
-- within the "interactive" namespace.
freshName :: Ident -> 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 :e and
-- loaded via :r.
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 a -> REPL a
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
getUserShowProverStats :: REPL Bool
-- | 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
data CommandExitCode
CommandOk :: CommandExitCode
CommandError :: CommandExitCode
-- | Parse a line as a command.
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
-- | Run a command.
runCommand :: Command -> REPL CommandExitCode
-- | Split at the first word boundary.
splitCommand :: String -> Maybe (String, String)
-- | Lookup a string in the command list.
findCommand :: String -> [CommandDescr]
-- | Lookup a string in the command list, returning an exact match even if
-- it's the prefix of another command.
findCommandExact :: String -> [CommandDescr]
-- | Lookup a string in the notebook-safe command list.
findNbCommand :: Bool -> String -> [CommandDescr]
moduleCmd :: String -> REPL ()
loadCmd :: FilePath -> REPL ()
loadPrelude :: REPL ()
setOptionCmd :: String -> REPL ()
interactiveConfig :: Config
replParseExpr :: String -> REPL (Expr PName)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)
-- | Randomly test a property, or exhaustively check it if the number of
-- values in the type under test is smaller than the tests
-- environment variable, or we specify exhaustive testing.
qcCmd :: QCMode -> String -> REPL [TestReport]
data QCMode
QCRandom :: QCMode
QCExhaust :: QCMode
satCmd :: String -> REPL ()
proveCmd :: String -> REPL ()
onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats)
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
handleCtrlC :: a -> REPL a
-- | Strip leading space.
sanitize :: String -> String
-- | Lift a parsing action into the REPL monad.
replParse :: (String -> Either ParseError a) -> String -> REPL a
liftModuleCmd :: ModuleCmd a -> REPL a
moduleCmdResult :: ModuleRes a -> REPL a
instance GHC.Show.Show Cryptol.REPL.Command.QCMode
instance GHC.Classes.Eq Cryptol.REPL.Command.QCMode
instance GHC.Show.Show Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Eq Cryptol.REPL.Command.CommandDescr
instance GHC.Classes.Ord Cryptol.REPL.Command.CommandDescr