cryptol-2.8.0: Cryptol: The Language of Cryptography

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 String
  }
- data DeclGroup
  - = Recursive [Decl]
  - | NonRecursive Decl
- data Match
  - = From Name Type Type Expr
  - | Let Decl
- data Expr
  - = EList [Expr] Type
  - | ETuple [Expr]
  - | ERec [(Ident, Expr)]
  - | ESel Expr Selector
  - | ESet 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
  - | EProofAbs Prop Expr
  - | EProofApp Expr
  - | EWhere Expr [DeclGroup]
- data ModVParam = ModVParam {
  - mvpName :: Name
  - mvpType :: Schema
  - mvpDoc :: Maybe String
  - mvpFixity :: Maybe Fixity
  }
- data ModTParam = ModTParam {
  - mtpName :: Name
  - mtpKind :: Kind
  - mtpNumber :: !Int
  - mtpDoc :: Maybe String
  }
- 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
  - = 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 Ident Name
  - primTypes :: Map Ident Name
  }
- data TCErrorMessage = TCErrorMessage {
  - tcErrorMessage :: !String
  }
- 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 Source # show :: DeclDef -> String Source # showList :: [DeclDef] -> ShowS Source #
Generic DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclDef :: Type -> Type Source # Methods from :: DeclDef -> Rep DeclDef x Source # to :: Rep DeclDef x -> DeclDef Source #
NFData DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: 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 #
TVars DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclDef -> DeclDef 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 String

#### Instances

Instances details

Show Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Decl -> ShowS Source # show :: Decl -> String Source # showList :: [Decl] -> ShowS Source #
Generic Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Decl :: Type -> Type Source # Methods from :: Decl -> Rep Decl x Source # to :: Rep Decl x -> Decl Source #
NFData Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Decl -> () Source #
PP Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Decl -> Doc 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 #
TVars Decl Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Decl -> Decl 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))))

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 Source # show :: DeclGroup -> String Source # showList :: [DeclGroup] -> ShowS Source #
Generic DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclGroup :: Type -> Type Source # Methods from :: DeclGroup -> Rep DeclGroup x Source # to :: Rep DeclGroup x -> DeclGroup Source #
NFData DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: DeclGroup -> () Source #
PP DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> DeclGroup -> Doc 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 #
TVars DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclGroup -> DeclGroup 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # show :: Match -> String Source # showList :: [Match] -> ShowS Source #
Generic Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Match :: Type -> Type Source # Methods from :: Match -> Rep Match x Source # to :: Rep Match x -> Match Source #
NFData Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Match -> () Source #
PP Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Match -> Doc 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 #
TVars Match Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Match -> Match 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 [(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 `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 Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
Generic Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Expr :: Type -> Type Source # Methods from :: Expr -> Rep Expr x Source # to :: Rep Expr x -> Expr Source #
NFData Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Expr -> () Source #
PP Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> Expr -> Doc 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 #
TVars Expr Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Expr -> Expr 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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]))))))

data ModVParam Source #

A value parameter of a module.

Constructors

ModVParam |

Fields

- mvpName :: Name
- mvpType :: Schema
- mvpDoc :: Maybe String
- mvpFixity :: Maybe Fixity

#### Instances

Instances details

Show ModVParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> ModVParam -> ShowS Source # show :: ModVParam -> String Source # showList :: [ModVParam] -> ShowS Source #
Generic ModVParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep ModVParam :: Type -> Type Source # Methods from :: ModVParam -> Rep ModVParam x Source # to :: Rep ModVParam x -> ModVParam Source #
NFData ModVParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: ModVParam -> () Source #
type Rep ModVParam Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

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 String

#### Instances

Instances details

Show ModTParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> ModTParam -> ShowS Source # show :: ModTParam -> String Source # showList :: [ModTParam] -> ShowS Source #
Generic ModTParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep ModTParam :: Type -> Type Source # Methods from :: ModTParam -> Rep ModTParam x Source # to :: Rep ModTParam x -> ModTParam Source #
NFData ModTParam Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: ModTParam -> () Source #
type Rep ModTParam Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

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 Source # show :: Module -> String Source # showList :: [Module] -> ShowS Source #
Generic Module Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Module :: Type -> Type Source # Methods from :: Module -> Rep Module x Source # to :: Rep Module x -> Module Source #
NFData Module Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Module -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 -> 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.

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 Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Show Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
Generic Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Name :: Type -> Type Source # Methods from :: Name -> Rep Name x Source # to :: Rep Name x -> Name Source #
NFData Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Name -> () Source #
PPName Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe (Assoc, Int) 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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # maxBound :: TFun Source #
Enum TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods succ :: TFun -> TFun Source # pred :: TFun -> TFun Source # toEnum :: Int -> TFun Source # fromEnum :: TFun -> Int Source # enumFrom :: TFun -> [TFun] Source # enumFromThen :: TFun -> TFun -> [TFun] Source # enumFromTo :: TFun -> TFun -> [TFun] Source # enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] Source #
Eq TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods (==) :: TFun -> TFun -> Bool Source # (/=) :: TFun -> TFun -> Bool Source #
Ord TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods compare :: TFun -> TFun -> Ordering Source # (<) :: TFun -> TFun -> Bool Source # (<=) :: TFun -> TFun -> Bool Source # (>) :: TFun -> TFun -> Bool Source # (>=) :: TFun -> TFun -> Bool Source # max :: TFun -> TFun -> TFun Source # min :: TFun -> TFun -> TFun Source #
Show TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods showsPrec :: Int -> TFun -> ShowS Source # show :: TFun -> String Source # showList :: [TFun] -> ShowS Source #
Generic TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Associated Types type Rep TFun :: Type -> Type Source # Methods from :: TFun -> Rep TFun x Source # to :: Rep TFun x -> TFun Source #
NFData TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods rnf :: TFun -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # (/=) :: Selector -> Selector -> Bool Source #
Ord Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods compare :: Selector -> Selector -> Ordering Source # (<) :: Selector -> Selector -> Bool Source # (<=) :: Selector -> Selector -> Bool Source # (>) :: Selector -> Selector -> Bool Source # (>=) :: Selector -> Selector -> Bool Source # max :: Selector -> Selector -> Selector Source # min :: Selector -> Selector -> Selector Source #
Show Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods showsPrec :: Int -> Selector -> ShowS Source # show :: Selector -> String Source # showList :: [Selector] -> ShowS Source #
Generic Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Associated Types type Rep Selector :: Type -> Type Source # Methods from :: Selector -> Rep Selector x Source # to :: Rep Selector x -> Selector Source #
NFData Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods rnf :: Selector -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # (/=) :: Import -> Import -> Bool Source #
Show Import Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Import -> ShowS Source # show :: Import -> String Source # showList :: [Import] -> ShowS Source #
Generic Import Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Import :: Type -> Type Source # Methods from :: Import -> Rep Import x Source # to :: Rep Import x -> Import Source #
NFData Import Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Import -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # (/=) :: ImportSpec -> ImportSpec -> Bool Source #
Show ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS Source # show :: ImportSpec -> String Source # showList :: [ImportSpec] -> ShowS Source #
Generic ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type Source # Methods from :: ImportSpec -> Rep ImportSpec x Source # to :: Rep ImportSpec x -> ImportSpec Source #
NFData ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # (/=) :: ExportType -> ExportType -> Bool Source #
Ord ExportType Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ExportType -> ExportType -> Ordering Source #

(<) :: ExportType -> ExportType -> Bool Source #

(<=) :: ExportType -> ExportType -> Bool Source #

(>) :: ExportType -> ExportType -> Bool Source #

(>=) :: ExportType -> ExportType -> Bool Source #

max :: ExportType -> ExportType -> ExportType Source #

min :: ExportType -> ExportType -> ExportType Source #

Show ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS Source # show :: ExportType -> String Source # showList :: [ExportType] -> ShowS Source #
Generic ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type Source # Methods from :: ExportType -> Rep ExportType x Source # to :: Rep ExportType x -> ExportType Source #
NFData ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () Source #
type Rep ExportType Source # |
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # show :: ExportSpec name -> String Source # showList :: [ExportSpec name] -> ShowS Source #
Generic (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Associated Types type Rep (ExportSpec name) :: Type -> Type Source # Methods from :: ExportSpec name -> Rep (ExportSpec name) x Source # to :: Rep (ExportSpec name) x -> ExportSpec name Source #
Ord name => Semigroup (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Methods (<>) :: ExportSpec name -> ExportSpec name -> ExportSpec name Source # sconcat :: NonEmpty (ExportSpec name) -> ExportSpec name Source # stimes :: Integral b => b -> ExportSpec name -> ExportSpec name Source #
Ord name => Monoid (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Methods mempty :: ExportSpec name Source # mappend :: ExportSpec name -> ExportSpec name -> ExportSpec name Source # mconcat :: [ExportSpec name] -> ExportSpec name Source #
NFData name => NFData (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Methods rnf :: ExportSpec name -> () Source #
type Rep (ExportSpec name) Source # |

Instance details

Defined in Cryptol.ModuleSystem.Exports

type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # (/=) :: Pragma -> Pragma -> Bool Source #
Show Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
Generic Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Pragma :: Type -> Type Source # Methods from :: Pragma -> Rep Pragma x Source # to :: Rep Pragma x -> Pragma Source #
NFData Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pragma -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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.Parser.Fixity Methods (==) :: Fixity -> Fixity -> Bool Source # (/=) :: Fixity -> Fixity -> Bool Source #
Show Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods showsPrec :: Int -> Fixity -> ShowS Source # show :: Fixity -> String Source # showList :: [Fixity] -> ShowS Source #
Generic Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Associated Types type Rep Fixity :: Type -> Type Source # Methods from :: Fixity -> Rep Fixity x Source # to :: Rep Fixity x -> Fixity Source #
NFData Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods rnf :: Fixity -> () Source #
PP Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods ppPrec :: Int -> Fixity -> Doc Source #
type Rep Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Ident Name
- primTypes :: Map Ident Name

#### Instances

Instances details

Show PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS Source # show :: PrimMap -> String Source # showList :: [PrimMap] -> ShowS Source #
Generic PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep PrimMap :: Type -> Type Source # Methods from :: PrimMap -> Rep PrimMap x Source # to :: Rep PrimMap x -> PrimMap Source #
NFData PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: PrimMap -> () Source #
type Rep PrimMap Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

- tcErrorMessage :: !String

#### Instances

Instances details

Eq TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods (==) :: TCErrorMessage -> TCErrorMessage -> Bool Source # (/=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #
Ord TCErrorMessage Source # |

Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TCErrorMessage -> TCErrorMessage -> Ordering Source #

(<) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(<=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(>) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(>=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

max :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage Source #

min :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage Source #

Show TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods showsPrec :: Int -> TCErrorMessage -> ShowS Source # show :: TCErrorMessage -> String Source # showList :: [TCErrorMessage] -> ShowS Source #
Generic TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Associated Types type Rep TCErrorMessage :: Type -> Type Source # Methods from :: TCErrorMessage -> Rep TCErrorMessage x Source # to :: Rep TCErrorMessage x -> TCErrorMessage Source #
NFData TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods rnf :: TCErrorMessage -> () Source #
PP TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods ppPrec :: Int -> TCErrorMessage -> Doc Source #
type Rep TCErrorMessage Source # |
Instance details Defined in Cryptol.TypeCheck.TCon type Rep TCErrorMessage = D1 ('MetaData "TCErrorMessage" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "TCErrorMessage" 'PrefixI 'True) (S1 ('MetaSel ('Just "tcErrorMessage") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)))

module Cryptol.TypeCheck.Type