cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.AST

Description

 
Synopsis

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

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

TVars DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

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

data Decl Source #

Constructors

Decl 

Fields

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 #

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

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 #

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

TVars DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

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

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 #

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

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

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 #

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

data ModVParam Source #

A value parameter of a module.

Constructors

ModVParam 

Fields

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

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

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

data Module Source #

A Cryptol module.

Constructors

Module 

Fields

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

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.

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 #

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

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

FromDecl (TopDecl Name) Source # 
Instance details

Defined in Cryptol.TypeCheck.Depends

type Rep Name Source # 
Instance details

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

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

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

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

data Import Source #

An import declaration.

Constructors

Import 

Fields

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

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

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

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

Fields

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

data Pragma Source #

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

data Fixity Source #

Constructors

Fixity 

Fields

Instances

Instances details
Eq Fixity Source # 
Instance details

Defined in Cryptol.Parser.Fixity

Methods

(==) :: Fixity -> Fixity -> Bool

(/=) :: Fixity -> Fixity -> Bool

Show Fixity Source # 
Instance details

Defined in Cryptol.Parser.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

Generic Fixity Source # 
Instance details

Defined in Cryptol.Parser.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.Parser.Fixity

Methods

rnf :: Fixity -> ()

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

data PrimMap Source #

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

Constructors

PrimMap 

Fields

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

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

Instances

Instances details
Eq TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Ord TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TCErrorMessage -> ShowS

show :: TCErrorMessage -> String

showList :: [TCErrorMessage] -> ShowS

Generic TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TCErrorMessage :: Type -> Type

NFData TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCErrorMessage -> ()

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-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "TCErrorMessage" 'PrefixI 'True) (S1 ('MetaSel ('Just "tcErrorMessage") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)))