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
- data Decl = Decl {}
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- data Match
- data Expr
- data ModVParam = ModVParam {}
- data ModTParam = ModTParam {}
- 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 -> Ident -> 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
- data Selector
- data Import = Import {}
- data ImportSpec
- data ExportType
- data ExportSpec name = ExportSpec {}
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- data Pragma
- data Fixity = Fixity {}
- data PrimMap = PrimMap {}
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- module Cryptol.TypeCheck.Type
Documentation
Instances
Show DeclDef Source # | |
Generic DeclDef Source # | |
NFData DeclDef Source # | |
Defined in Cryptol.TypeCheck.AST | |
ShowParseable DeclDef Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclDef -> Doc Source # | |
FreeVars DeclDef Source # | |
TVars DeclDef Source # | |
PP (WithNames DeclDef) Source # | |
type Rep DeclDef Source # | |
Defined in Cryptol.TypeCheck.AST type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) |
Constructors
Decl | |
Instances
Show Decl Source # | |
Generic Decl Source # | |
NFData Decl Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP Decl Source # | |
ShowParseable Decl Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Decl -> Doc Source # | |
Defs Decl Source # | |
FreeVars Decl Source # | |
TVars Decl Source # | |
PP (WithNames Decl) Source # | |
type Rep Decl Source # | |
Defined in Cryptol.TypeCheck.AST type Rep Decl = D1 ('MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String)))))) |
Constructors
Recursive [Decl] | Mutually recursive declarations |
NonRecursive Decl | Non-recursive declaration |
Instances
Show DeclGroup Source # | |
Generic DeclGroup Source # | |
NFData DeclGroup Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP DeclGroup Source # | |
ShowParseable DeclGroup Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclGroup -> Doc Source # | |
Defs DeclGroup Source # | |
FreeVars DeclGroup Source # | |
TVars DeclGroup Source # | |
PP (WithNames DeclGroup) Source # | |
type Rep DeclGroup Source # | |
Defined in Cryptol.TypeCheck.AST type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))) |
Constructors
From Name Type Type Expr | Type arguments are the length and element type of the sequence expression |
Let Decl |
Instances
Show Match Source # | |
Generic Match Source # | |
NFData Match Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP Match Source # | |
ShowParseable Match Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Match -> Doc Source # | |
Defs Match Source # | |
FreeVars Match Source # | |
TVars Match Source # | |
PP (WithNames Match) Source # | |
type Rep Match Source # | |
Defined in Cryptol.TypeCheck.AST type Rep Match = D1 ('MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))) |
Constructors
EList [Expr] Type | List value (with type of elements) |
ETuple [Expr] | Tuple value |
ERec [(Ident, Expr)] | Record value |
ESel Expr Selector | Elimination for tuplerecordlist |
ESet Expr Selector Expr | Change the value of a field. |
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 |
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 |
EProofApp Expr | If `e : p => t`, then `EProofApp e : t`,
as long as we can prove 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
Show Expr Source # | |
Generic Expr Source # | |
NFData Expr Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP Expr Source # | |
ShowParseable Expr Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Expr -> Doc Source # | |
FreeVars Expr Source # | |
TVars Expr Source # | |
PP (WithNames Expr) Source # | |
type Rep Expr Source # | |
Defined in Cryptol.TypeCheck.AST type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 [(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 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 "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])))))) |
A value parameter of a module.
Constructors
ModVParam | |
Instances
Show ModVParam Source # | |
Generic ModVParam Source # | |
NFData ModVParam Source # | |
Defined in Cryptol.TypeCheck.AST | |
type Rep ModVParam Source # | |
Defined in Cryptol.TypeCheck.AST type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String)) :*: S1 ('MetaSel ('Just "mvpFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity))))) |
A type parameter of a module.
Constructors
ModTParam | |
Instances
Show ModTParam Source # | |
Generic ModTParam Source # | |
NFData ModTParam Source # | |
Defined in Cryptol.TypeCheck.AST | |
type Rep ModTParam Source # | |
Defined in Cryptol.TypeCheck.AST type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String))))) |
A Cryptol module.
Constructors
Module | |
Fields
|
Instances
Show Module Source # | |
Generic Module Source # | |
NFData Module Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP Module Source # | |
TVars Module Source # | |
PP (WithNames Module) Source # | |
type Rep Module Source # | |
Defined in Cryptol.TypeCheck.AST type Rep Module = D1 ('MetaData "Module" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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?
groupDecls :: DeclGroup -> [Decl] Source #
ePrim :: PrimMap -> Ident -> Expr Source #
Construct a primitive, given a map to the unique names of the Cryptol module.
eError :: PrimMap -> Type -> String -> Expr Source #
Make an expression that is error
pre-applied to a type and a message.
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) 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.
Instances
Eq Name Source # | |
Ord Name Source # | |
Show Name Source # | |
Generic Name Source # | |
NFData Name Source # | |
Defined in Cryptol.ModuleSystem.Name | |
PPName Name Source # | |
Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe (Assoc, Int) Source # ppPrefixName :: Name -> Doc Source # ppInfixName :: Name -> Doc Source # | |
PP Name Source # | |
ShowParseable Name Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Name -> Doc Source # | |
FromDecl (Decl Name) Source # | |
Defined in Cryptol.TypeCheck.Depends | |
FromDecl (TopDecl Name) Source # | |
Defined in Cryptol.TypeCheck.Depends | |
type Rep Name Source # | |
Defined in Cryptol.ModuleSystem.Name type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
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 |
|
Instances
Bounded TFun Source # | |
Defined in Cryptol.TypeCheck.TCon | |
Enum TFun Source # | |
Eq TFun Source # | |
Ord TFun Source # | |
Show TFun Source # | |
Generic TFun Source # | |
NFData TFun Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP TFun Source # | |
HasKind TFun Source # | |
type Rep TFun Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
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
Eq Selector Source # | |
Ord Selector Source # | |
Defined in Cryptol.Parser.Selector | |
Show Selector Source # | |
Generic Selector Source # | |
NFData Selector Source # | |
Defined in Cryptol.Parser.Selector | |
PP Selector Source # | |
ShowParseable Selector Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Selector -> Doc Source # | |
type Rep Selector Source # | |
Defined in Cryptol.Parser.Selector type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
An import declaration.
Instances
Eq Import Source # | |
Show Import Source # | |
Generic Import Source # | |
NFData Import Source # | |
Defined in Cryptol.Parser.AST | |
PP Import Source # | |
type Rep Import Source # | |
Defined in Cryptol.Parser.AST type Rep Import = D1 ('MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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.
Instances
Eq ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
Show ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS show :: ImportSpec -> String showList :: [ImportSpec] -> ShowS | |
Generic ImportSpec Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type | |
NFData ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () | |
PP ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source # | |
type Rep ImportSpec Source # | |
Defined in Cryptol.Parser.AST type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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.
Instances
Eq ExportType Source # | |
Defined in Cryptol.Parser.AST | |
Ord ExportType Source # | |
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 # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS show :: ExportType -> String showList :: [ExportType] -> ShowS | |
Generic ExportType Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type | |
NFData ExportType Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () | |
type Rep ExportType Source # | |
Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type)) |
data ExportSpec name Source #
Constructors
ExportSpec | |
Instances
Show name => Show (ExportSpec name) Source # | |
Defined in Cryptol.ModuleSystem.Exports Methods showsPrec :: Int -> ExportSpec name -> ShowS show :: ExportSpec name -> String showList :: [ExportSpec name] -> ShowS | |
Generic (ExportSpec name) Source # | |
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 # | |
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 # | |
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 # | |
Defined in Cryptol.ModuleSystem.Exports Methods rnf :: ExportSpec name -> () | |
type Rep (ExportSpec name) Source # | |
Defined in Cryptol.ModuleSystem.Exports type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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.
Constructors
PragmaNote String | |
PragmaProperty |
Instances
Eq Pragma Source # | |
Show Pragma Source # | |
Generic Pragma Source # | |
NFData Pragma Source # | |
Defined in Cryptol.Parser.AST | |
PP Pragma Source # | |
NoPos Pragma Source # | |
type Rep Pragma Source # | |
Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type)) |
Instances
Eq Fixity Source # | |
Show Fixity Source # | |
Generic Fixity Source # | |
NFData Fixity Source # | |
Defined in Cryptol.Parser.Fixity | |
PP Fixity Source # | |
type Rep Fixity Source # | |
Defined in Cryptol.Parser.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) |
A mapping from an identifier defined in some module to its real name.
Instances
Show PrimMap Source # | |
Generic PrimMap Source # | |
NFData PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name | |
type Rep PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "PrimMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "primDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident Name)) :*: S1 ('MetaSel ('Just "primTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident Name)))) |
data TCErrorMessage Source #
Constructors
TCErrorMessage | |
Fields
|
Instances
module Cryptol.TypeCheck.Type