Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.AST

Description

Synopsis

data DeclDef
- = DPrim
- | DExpr Expr
data Decl = Decl {
- dName :: !Name
- dSignature :: Schema
- dDefinition :: DeclDef
- dPragmas :: [Pragma]
- dInfix :: !Bool
- dFixity :: Maybe Fixity
- dDoc :: Maybe Text
}
data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
data Match
- = From Name Type Type Expr
- | Let Decl
data Expr
- = EList [Expr] Type
- | ETuple [Expr]
- | ERec (RecordMap Ident Expr)
- | ESel Expr Selector
- | ESet Type Expr Selector Expr
- | EIf Expr Expr Expr
- | EComp Type Type Expr [[Match]]
- | EVar Name
- | ETAbs TParam Expr
- | ETApp Expr Type
- | EApp Expr Expr
- | EAbs Name Type Expr
- | ELocated Range Expr
- | EProofAbs Prop Expr
- | EProofApp Expr
- | EWhere Expr [DeclGroup]
data ModVParam = ModVParam {
- mvpName :: Name
- mvpType :: Schema
- mvpDoc :: Maybe Text
- mvpFixity :: Maybe Fixity
}
data ModTParam = ModTParam {
- mtpName :: Name
- mtpKind :: Kind
- mtpNumber :: !Int
- mtpDoc :: Maybe Text
}
data Module = Module {
- mName :: !ModName
- mExports :: ExportSpec Name
- mImports :: [Import]
- mTySyns :: Map Name TySyn
- mNewtypes :: Map Name Newtype
- mPrimTypes :: Map Name AbstractType
- mParamTypes :: Map Name ModTParam
- mParamConstraints :: [Located Prop]
- mParamFuns :: Map Name ModVParam
- mDecls :: [DeclGroup]
}
isParametrizedModule :: Module -> Bool
mtpParam :: ModTParam -> TParam
groupDecls :: DeclGroup -> [Decl]
ePrim :: PrimMap -> PrimIdent -> Expr
eError :: PrimMap -> Type -> String -> Expr
eString :: PrimMap -> String -> Expr
eChar :: PrimMap -> Char -> Expr
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitAbs :: Expr -> Maybe ((Name, Type), Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitTApp :: Expr -> Maybe (Type, Expr)
splitProofApp :: Expr -> Maybe ((), Expr)
splitExprInst :: Expr -> (Expr, [Type], Int)
data Name
data TFun
- = TCAdd
- | TCSub
- | TCMul
- | TCDiv
- | TCMod
- | TCExp
- | TCWidth
- | TCMin
- | TCMax
- | TCCeilDiv
- | TCCeilMod
- | TCLenFromThenTo
data Selector
- = TupleSel Int (Maybe Int)
- | RecordSel Ident (Maybe [Ident])
- | ListSel Int (Maybe Int)
data Import = Import {
- iModule :: !ModName
- iAs :: Maybe ModName
- iSpec :: Maybe ImportSpec
}
data ImportSpec
- = Hiding [Ident]
- | Only [Ident]
data ExportType
- = Public
- | Private
data ExportSpec name = ExportSpec {
- eTypes :: Set name
- eBinds :: Set name
}
isExportedBind :: Ord name => name -> ExportSpec name -> Bool
isExportedType :: Ord name => name -> ExportSpec name -> Bool
data Pragma
- = PragmaNote String
- | PragmaProperty
data Fixity = Fixity {
- fAssoc :: !Assoc
- fLevel :: !Int
}
data PrimMap = PrimMap {
- primDecls :: Map PrimIdent Name
- primTypes :: Map PrimIdent Name
}
module Cryptol.TypeCheck.Type

Documentation

data DeclDef Source #

Constructors

DPrim
DExpr Expr

Instances

Instances details

Show DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> DeclDef -> ShowS # show :: DeclDef -> String # showList :: [DeclDef] -> ShowS #
Generic DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclDef :: Type -> Type # Methods from :: DeclDef -> Rep DeclDef x # to :: Rep DeclDef x -> DeclDef #
NFData DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: DeclDef -> () #
TVars DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclDef -> DeclDef Source #
ShowParseable DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclDef -> Doc Source #
FreeVars DeclDef Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: DeclDef -> Deps Source #
PP (WithNames DeclDef) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames DeclDef -> Doc Source #
type Rep DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))

data Decl Source #

Constructors

Decl
Fields dName :: !Name dSignature :: Schema dDefinition :: DeclDef dPragmas :: [Pragma] dInfix :: !Bool dFixity :: Maybe Fixity dDoc :: Maybe Text

Instances

Instances details

Show Decl Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Decl -> ShowS # show :: Decl -> String # showList :: [Decl] -> ShowS #
Generic Decl Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Decl :: Type -> Type # Methods from :: Decl -> Rep Decl x # to :: Rep Decl x -> Decl #
NFData Decl Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Decl -> () #
PP Decl Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Decl -> Doc Source #
TVars Decl Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Decl -> Decl Source #
ShowParseable Decl Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Decl -> Doc Source #
Defs Decl Source #
Instance details Defined in Cryptol.IR.FreeVars Methods defs :: Decl -> Set Name Source #
FreeVars Decl Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Decl -> Deps Source #
PP (WithNames Decl) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Decl -> Doc Source #
type Rep Decl Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep Decl = D1 ('MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Decl" 'PrefixI 'True) ((S1 ('MetaSel ('Just "dName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :: (S1 ('MetaSel ('Just "dSignature") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema) :: S1 ('MetaSel ('Just "dDefinition") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclDef))) :: ((S1 ('MetaSel ('Just "dPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pragma]) :: S1 ('MetaSel ('Just "dInfix") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "dFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :: S1 ('MetaSel ('Just "dDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data DeclGroup Source #

Constructors

Recursive [Decl]	Mutually recursive declarations
NonRecursive Decl	Non-recursive declaration

Instances

Instances details

Show DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> DeclGroup -> ShowS # show :: DeclGroup -> String # showList :: [DeclGroup] -> ShowS #
Generic DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclGroup :: Type -> Type # Methods from :: DeclGroup -> Rep DeclGroup x # to :: Rep DeclGroup x -> DeclGroup #
NFData DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: DeclGroup -> () #
PP DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> DeclGroup -> Doc Source #
TVars DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclGroup -> DeclGroup Source #
ShowParseable DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclGroup -> Doc Source #
Defs DeclGroup Source #
Instance details Defined in Cryptol.IR.FreeVars Methods defs :: DeclGroup -> Set Name Source #
FreeVars DeclGroup Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: DeclGroup -> Deps Source #
PP (WithNames DeclGroup) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames DeclGroup -> Doc Source #
type Rep DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Recursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Decl])) :+: C1 ('MetaCons "NonRecursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Decl)))

data Match Source #

Constructors

From Name Type Type Expr	Type arguments are the length and element type of the sequence expression
Let Decl

Instances

Instances details

Show Match Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Match -> ShowS # show :: Match -> String # showList :: [Match] -> ShowS #
Generic Match Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Match :: Type -> Type # Methods from :: Match -> Rep Match x # to :: Rep Match x -> Match #
NFData Match Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Match -> () #
PP Match Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Match -> Doc Source #
TVars Match Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Match -> Match Source #
ShowParseable Match Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Match -> Doc Source #
Defs Match Source #
Instance details Defined in Cryptol.IR.FreeVars Methods defs :: Match -> Set Name Source #
FreeVars Match Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Match -> Deps Source #
PP (WithNames Match) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Match -> Doc Source #
type Rep Match Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep Match = D1 ('MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "From" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Decl)))

data Expr Source #

Constructors

EList [Expr] Type	List value (with type of elements)
ETuple [Expr]	Tuple value
ERec (RecordMap Ident Expr)	Record value
ESel Expr Selector	Elimination for tuplerecordlist
ESet Type Expr Selector Expr	Change the value of a field. The included type gives the type of the record being updated
EIf Expr Expr Expr	If-then-else
EComp Type Type Expr [[Match]]	List comprehensions The types cache the length of the sequence and its element type.
EVar Name	Use of a bound variable
ETAbs TParam Expr	Function Value
ETApp Expr Type	Type application
EApp Expr Expr	Function application
EAbs Name Type Expr	Function value
ELocated Range Expr	Source location information
EProofAbs Prop 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`.
EProofApp 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.
EWhere Expr [DeclGroup]

Instances

Instances details

Show Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Generic Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Expr :: Type -> Type # Methods from :: Expr -> Rep Expr x # to :: Rep Expr x -> Expr #
NFData Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Expr -> () #
PP Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Expr -> Doc Source #
HasLoc Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods getLoc :: Expr -> Maybe Range Source #
TVars Expr Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Expr -> Expr Source #
ShowParseable Expr Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Expr -> Doc Source #
FreeVars Expr Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Expr -> Deps Source #
PP (WithNames Expr) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Expr -> Doc Source #
type Rep Expr Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) ((((C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: (C1 ('MetaCons "ERec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Expr))) :+: C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)))) :+: ((C1 ('MetaCons "ESet" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "EComp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match]]))) :+: C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "ELocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EProofAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "EProofApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]))))))

data ModVParam Source #

A value parameter of a module.

Constructors

ModVParam
Fields mvpName :: Name mvpType :: Schema mvpDoc :: Maybe Text mvpFixity :: Maybe Fixity

Instances

Instances details

Show ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> ModVParam -> ShowS # show :: ModVParam -> String # showList :: [ModVParam] -> ShowS #
Generic ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep ModVParam :: Type -> Type # Methods from :: ModVParam -> Rep ModVParam x # to :: Rep ModVParam x -> ModVParam #
NFData ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: ModVParam -> () #
type Rep ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "ModVParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mvpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "mvpType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema)) :: (S1 ('MetaSel ('Just "mvpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "mvpFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)))))

data ModTParam Source #

A type parameter of a module.

Constructors

ModTParam
Fields mtpName :: Name mtpKind :: Kind mtpNumber :: !Int The number of the parameter in the module This is used when we move parameters from the module level to individual declarations (type synonyms in particular) mtpDoc :: Maybe Text

Instances

Instances details

Show ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> ModTParam -> ShowS # show :: ModTParam -> String # showList :: [ModTParam] -> ShowS #
Generic ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep ModTParam :: Type -> Type # Methods from :: ModTParam -> Rep ModTParam x # to :: Rep ModTParam x -> ModTParam #
NFData ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: ModTParam -> () #
type Rep ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "ModTParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mtpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "mtpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Just "mtpNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "mtpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)))))

data Module Source #

A Cryptol module.

Constructors

Module
Fields mName :: !ModName mExports :: ExportSpec Name mImports :: [Import] mTySyns :: Map Name TySyn This is just the type-level type synonyms of a module. mNewtypes :: Map Name Newtype mPrimTypes :: Map Name AbstractType mParamTypes :: Map Name ModTParam mParamConstraints :: [Located Prop] mParamFuns :: Map Name ModVParam mDecls :: [DeclGroup]

Instances

Instances details

Show Module Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Module -> ShowS # show :: Module -> String # showList :: [Module] -> ShowS #
Generic Module Source #
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Module :: Type -> Type # Methods from :: Module -> Rep Module x # to :: Rep Module x -> Module #
NFData Module Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Module -> () #
PP Module Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Module -> Doc Source #
TVars Module Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Module -> Module Source #
PP (WithNames Module) Source #
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Module -> Doc Source #
type Rep Module Source #
Instance details Defined in Cryptol.TypeCheck.AST type Rep Module = D1 ('MetaData "Module" "Cryptol.TypeCheck.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :: S1 ('MetaSel ('Just "mExports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExportSpec Name))) :: (S1 ('MetaSel ('Just "mImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Import]) :: (S1 ('MetaSel ('Just "mTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :: S1 ('MetaSel ('Just "mNewtypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name Newtype))))) :: ((S1 ('MetaSel ('Just "mPrimTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name AbstractType)) :: S1 ('MetaSel ('Just "mParamTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam))) :: (S1 ('MetaSel ('Just "mParamConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :: (S1 ('MetaSel ('Just "mParamFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam)) :*: S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]))))))

isParametrizedModule :: Module -> Bool Source #

Is this a parameterized module?

mtpParam :: ModTParam -> TParam Source #

groupDecls :: DeclGroup -> [Decl] Source #

ePrim :: PrimMap -> PrimIdent -> Expr Source #

Construct a primitive, given a map to the unique primitive name.

eError :: PrimMap -> Type -> String -> Expr Source #

Make an expression that is error pre-applied to a type and a message.

eString :: PrimMap -> String -> Expr Source #

eChar :: PrimMap -> Char -> Expr Source #

ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc Source #

splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source #

splitAbs :: Expr -> Maybe ((Name, Type), Expr) Source #

splitTAbs :: Expr -> Maybe (TParam, Expr) Source #

splitProofAbs :: Expr -> Maybe (Prop, Expr) Source #

splitTApp :: Expr -> Maybe (Type, Expr) Source #

splitProofApp :: Expr -> Maybe ((), Expr) Source #

splitExprInst :: Expr -> (Expr, [Type], Int) Source #

Deconstruct an expression, typically polymorphic, into the types and proofs to which it is applied. Since we don't store the proofs, we just return the number of proof applications. The first type is the one closest to the expr.

data Name Source #

Instances

Instances details

Eq Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Show Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
Generic Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Name :: Type -> Type # Methods from :: Name -> Rep Name x # to :: Rep Name x -> Name #
NFData Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Name -> () #
PPName Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe Fixity Source # ppPrefixName :: Name -> Doc Source # ppInfixName :: Name -> Doc Source #
PP Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppPrec :: Int -> Name -> Doc Source #
ShowParseable Name Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Name -> Doc Source #
FromDecl (Decl Name) Source #
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: Decl Name -> Maybe (Bind Name) Source # toParamFun :: Decl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: Decl Name -> [Located (Prop Name)] Source # toTyDecl :: Decl Name -> Maybe TyDecl Source # isTopDecl :: Decl Name -> Bool Source #
FromDecl (TopDecl Name) Source #
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: TopDecl Name -> Maybe (Bind Name) Source # toParamFun :: TopDecl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: TopDecl Name -> [Located (Prop Name)] Source # toTyDecl :: TopDecl Name -> Maybe TyDecl Source # isTopDecl :: TopDecl Name -> Bool Source #
type Rep Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Name" 'PrefixI 'True) ((S1 ('MetaSel ('Just "nUnique") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "nInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NameInfo)) :: (S1 ('MetaSel ('Just "nIdent") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident) :: (S1 ('MetaSel ('Just "nFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :: S1 ('MetaSel ('Just "nLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range)))))

data TFun Source #

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

Constructors

TCAdd	: Num -> Num -> Num
TCSub	: Num -> Num -> Num
TCMul	: Num -> Num -> Num
TCDiv	: Num -> Num -> Num
TCMod	: Num -> Num -> Num
TCExp	: Num -> Num -> Num
TCWidth	: Num -> Num
TCMin	: Num -> Num -> Num
TCMax	: Num -> Num -> Num
TCCeilDiv	: Num -> Num -> Num
TCCeilMod	: Num -> Num -> Num
TCLenFromThenTo	`: Num -> Num -> Num -> Num` Example: `[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]`

Instances

Instances details

Bounded TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods minBound :: TFun # maxBound :: TFun #
Enum TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods succ :: TFun -> TFun # pred :: TFun -> TFun # toEnum :: Int -> TFun # fromEnum :: TFun -> Int # enumFrom :: TFun -> [TFun] # enumFromThen :: TFun -> TFun -> [TFun] # enumFromTo :: TFun -> TFun -> [TFun] # enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] #
Eq TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods (==) :: TFun -> TFun -> Bool # (/=) :: TFun -> TFun -> Bool #
Ord TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods compare :: TFun -> TFun -> Ordering # (<) :: TFun -> TFun -> Bool # (<=) :: TFun -> TFun -> Bool # (>) :: TFun -> TFun -> Bool # (>=) :: TFun -> TFun -> Bool # max :: TFun -> TFun -> TFun # min :: TFun -> TFun -> TFun #
Show TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods showsPrec :: Int -> TFun -> ShowS # show :: TFun -> String # showList :: [TFun] -> ShowS #
Generic TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Associated Types type Rep TFun :: Type -> Type # Methods from :: TFun -> Rep TFun x # to :: Rep TFun x -> TFun #
NFData TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods rnf :: TFun -> () #
PP TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods ppPrec :: Int -> TFun -> Doc Source #
HasKind TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon Methods kindOf :: TFun -> Kind Source #
type Rep TFun Source #
Instance details Defined in Cryptol.TypeCheck.TCon type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (((C1 ('MetaCons "TCAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMul" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCExp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TCWidth" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMax" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCCeilDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCCeilMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCLenFromThenTo" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Selector Source #

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.

Constructors

TupleSel Int (Maybe Int)	Zero-based tuple selection. Optionally specifies the shape of the tuple (one-based).
RecordSel Ident (Maybe [Ident])	Record selection. Optionally specifies the shape of the record.
ListSel Int (Maybe Int)	List selection. Optionally specifies the length of the list.

Instances

Instances details

Eq Selector Source #
Instance details Defined in Cryptol.Parser.Selector Methods (==) :: Selector -> Selector -> Bool # (/=) :: Selector -> Selector -> Bool #
Ord Selector Source #
Instance details Defined in Cryptol.Parser.Selector Methods compare :: Selector -> Selector -> Ordering # (<) :: Selector -> Selector -> Bool # (<=) :: Selector -> Selector -> Bool # (>) :: Selector -> Selector -> Bool # (>=) :: Selector -> Selector -> Bool # max :: Selector -> Selector -> Selector # min :: Selector -> Selector -> Selector #
Show Selector Source #
Instance details Defined in Cryptol.Parser.Selector Methods showsPrec :: Int -> Selector -> ShowS # show :: Selector -> String # showList :: [Selector] -> ShowS #
Generic Selector Source #
Instance details Defined in Cryptol.Parser.Selector Associated Types type Rep Selector :: Type -> Type # Methods from :: Selector -> Rep Selector x # to :: Rep Selector x -> Selector #
NFData Selector Source #
Instance details Defined in Cryptol.Parser.Selector Methods rnf :: Selector -> () #
PP Selector Source #
Instance details Defined in Cryptol.Parser.Selector Methods ppPrec :: Int -> Selector -> Doc Source #
ShowParseable Selector Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Selector -> Doc Source #
type Rep Selector Source #
Instance details Defined in Cryptol.Parser.Selector type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "TupleSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))) :+: (C1 ('MetaCons "RecordSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Ident]))) :+: C1 ('MetaCons "ListSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))))

data Import Source #

An import declaration.

Constructors

Import
Fields iModule :: !ModName iAs :: Maybe ModName iSpec :: Maybe ImportSpec

Instances

Instances details

Eq Import Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Import -> Import -> Bool # (/=) :: Import -> Import -> Bool #
Show Import Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Import -> ShowS # show :: Import -> String # showList :: [Import] -> ShowS #
Generic Import Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Import :: Type -> Type # Methods from :: Import -> Rep Import x # to :: Rep Import x -> Import #
NFData Import Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Import -> () #
PP Import Source #
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Import -> Doc Source #
type Rep Import Source #
Instance details Defined in Cryptol.Parser.AST type Rep Import = D1 ('MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) (S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :: (S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName)) :: S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)))))

data ImportSpec Source #

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.

Constructors

Hiding [Ident]
Only [Ident]

Instances

Instances details

Eq ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImportSpec -> ImportSpec -> Bool # (/=) :: ImportSpec -> ImportSpec -> Bool #
Show ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS # show :: ImportSpec -> String # showList :: [ImportSpec] -> ShowS #
Generic ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type # Methods from :: ImportSpec -> Rep ImportSpec x # to :: Rep ImportSpec x -> ImportSpec #
NFData ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () #
PP ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source #
type Rep ImportSpec Source #
Instance details Defined in Cryptol.Parser.AST type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Hiding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])) :+: C1 ('MetaCons "Only" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])))

data ExportType Source #

Export information for a declaration.

Constructors

Public
Private

Instances

Instances details

Eq ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ExportType -> ExportType -> Bool # (/=) :: ExportType -> ExportType -> Bool #
Ord ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods compare :: ExportType -> ExportType -> Ordering # (<) :: ExportType -> ExportType -> Bool # (<=) :: ExportType -> ExportType -> Bool # (>) :: ExportType -> ExportType -> Bool # (>=) :: ExportType -> ExportType -> Bool # max :: ExportType -> ExportType -> ExportType # min :: ExportType -> ExportType -> ExportType #
Show ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS #
Generic ExportType Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type # Methods from :: ExportType -> Rep ExportType x # to :: Rep ExportType x -> ExportType #
NFData ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () #
type Rep ExportType Source #
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type))

data ExportSpec name Source #

Constructors

ExportSpec
Fields eTypes :: Set name eBinds :: Set name

Instances

Instances details

Show name => Show (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports Methods showsPrec :: Int -> ExportSpec name -> ShowS # show :: ExportSpec name -> String # showList :: [ExportSpec name] -> ShowS #
Generic (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports Associated Types type Rep (ExportSpec name) :: Type -> Type # Methods from :: ExportSpec name -> Rep (ExportSpec name) x # to :: Rep (ExportSpec name) x -> ExportSpec name #
Ord name => Semigroup (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports Methods (<>) :: ExportSpec name -> ExportSpec name -> ExportSpec name # sconcat :: NonEmpty (ExportSpec name) -> ExportSpec name # stimes :: Integral b => b -> ExportSpec name -> ExportSpec name #
Ord name => Monoid (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports Methods mempty :: ExportSpec name # mappend :: ExportSpec name -> ExportSpec name -> ExportSpec name # mconcat :: [ExportSpec name] -> ExportSpec name #
NFData name => NFData (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports Methods rnf :: ExportSpec name -> () #
type Rep (ExportSpec name) Source #
Instance details Defined in Cryptol.ModuleSystem.Exports type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "ExportSpec" 'PrefixI 'True) (S1 ('MetaSel ('Just "eTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set name)) :*: S1 ('MetaSel ('Just "eBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set name))))

isExportedBind :: Ord name => name -> ExportSpec name -> Bool Source #

Check to see if a binding is exported.

isExportedType :: Ord name => name -> ExportSpec name -> Bool Source #

Check to see if a type synonym is exported.

data Pragma Source #

Constructors

PragmaNote String
PragmaProperty

Instances

Instances details

Eq Pragma Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
Show Pragma Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
Generic Pragma Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Pragma :: Type -> Type # Methods from :: Pragma -> Rep Pragma x # to :: Rep Pragma x -> Pragma #
NFData Pragma Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pragma -> () #
PP Pragma Source #
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pragma -> Doc Source #
NoPos Pragma Source #
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pragma -> Pragma Source #
type Rep Pragma Source #
Instance details Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type))

data Fixity Source #

Constructors

Fixity
Fields fAssoc :: !Assoc fLevel :: !Int

Instances

Instances details

Eq Fixity Source #
Instance details Defined in Cryptol.Utils.Fixity Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Show Fixity Source #
Instance details Defined in Cryptol.Utils.Fixity Methods showsPrec :: Int -> Fixity -> ShowS # show :: Fixity -> String # showList :: [Fixity] -> ShowS #
Generic Fixity Source #
Instance details Defined in Cryptol.Utils.Fixity Associated Types type Rep Fixity :: Type -> Type # Methods from :: Fixity -> Rep Fixity x # to :: Rep Fixity x -> Fixity #
NFData Fixity Source #
Instance details Defined in Cryptol.Utils.Fixity Methods rnf :: Fixity -> () #
PP Fixity Source #
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Fixity -> Doc Source #
type Rep Fixity Source #
Instance details Defined in Cryptol.Utils.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

data PrimMap Source #

A mapping from an identifier defined in some module to its real name.

Constructors

PrimMap
Fields primDecls :: Map PrimIdent Name primTypes :: Map PrimIdent Name

Instances

Instances details

Show PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS # show :: PrimMap -> String # showList :: [PrimMap] -> ShowS #
Generic PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep PrimMap :: Type -> Type # Methods from :: PrimMap -> Rep PrimMap x # to :: Rep PrimMap x -> PrimMap #
Semigroup PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (<>) :: PrimMap -> PrimMap -> PrimMap # sconcat :: NonEmpty PrimMap -> PrimMap # stimes :: Integral b => b -> PrimMap -> PrimMap #
NFData PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: PrimMap -> () #
type Rep PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "PrimMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "primDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name)) :*: S1 ('MetaSel ('Just "primTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name))))

module Cryptol.TypeCheck.Type