cryptol-3.2.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 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
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 #

Show Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Match -> ShowS #

show :: Match -> String #

showList :: [Match] -> ShowS #

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 #

TraverseNames Match Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Match -> f Match Source #

ShowParseable Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Match -> Match Source #

PP Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Match -> Doc Source #

NFData Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Match -> () #

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

data Expr Source #

Constructors

EList [Expr] Type

List value (with type of elements)

ETuple [Expr]

Tuple value

ERec (RecordMap Ident Expr)

Record value

ESel Expr Selector

Elimination for tuplerecordlist

ESet Type Expr Selector Expr

Change the value of a field. The included type gives the type of the record being updated

EIf Expr Expr Expr

If-then-else

ECase Expr (Map Ident CaseAlt) (Maybe CaseAlt)

Case expression. The keys are the name of constructors Nothing for default case, the expresssions are what to do if the constructor matches. If the constructor binds variables, then then the expr should be EAbs

EComp Type Type Expr [[Match]]

List comprehensions The types cache the length of the sequence and its element type.

EVar Name

Use of a bound variable

ETAbs TParam Expr

Function Value

ETApp Expr Type

Type application

EApp Expr Expr

Function application

EAbs Name Type Expr

Function value

ELocated Range Expr

Source location information

EProofAbs Prop Expr

Proof abstraction. Because we don't keep proofs around we don't need to name the assumption, but we still need to record the assumption. The assumption is the Type term, which should be of kind KProp.

EProofApp Expr

If e : p => t, then EProofApp e : t, as long as we can prove p.

We don't record the actual proofs, as they are not used for anything. It may be nice to keep them around for sanity checking.

EWhere Expr [DeclGroup] 
EPropGuards [([Prop], Expr)] Type 

Instances

Instances details
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 #

Show Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

FreeVars Expr Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Expr -> Deps Source #

TraverseNames Expr Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Expr -> f Expr Source #

HasLoc Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

getLoc :: Expr -> Maybe Range Source #

ShowParseable Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Expr -> Expr Source #

PP Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Expr -> Doc Source #

NFData Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Expr -> () #

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-3.2.0-35bDsq0QUVdvBXha47jji" 'False) ((((C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: (C1 ('MetaCons "ERec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Expr))) :+: C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)))) :+: ((C1 ('MetaCons "ESet" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ECase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident CaseAlt)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe CaseAlt)))) :+: (C1 ('MetaCons "EComp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match]]))) :+: C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "ELocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EProofAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "EProofApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: (C1 ('MetaCons "EWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup])) :+: C1 ('MetaCons "EPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [([Prop], Expr)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))))

data ModuleG mname Source #

A Cryptol module.

Constructors

Module 

Fields

Instances

Instances details
Generic (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep (ModuleG mname) :: Type -> Type #

Methods

from :: ModuleG mname -> Rep (ModuleG mname) x #

to :: Rep (ModuleG mname) x -> ModuleG mname #

Show mname => Show (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> ModuleG mname -> ShowS #

show :: ModuleG mname -> String #

showList :: [ModuleG mname] -> ShowS #

ModuleInstance (ModuleG name) Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: ModuleG name -> ModuleG name Source #

TVars (ModuleG names) Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> ModuleG names -> ModuleG names Source #

PP n => PP (ModuleG n) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> ModuleG n -> Doc Source #

PP n => PP (WithNames (ModuleG n)) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames (ModuleG n) -> Doc Source #

NFData mname => NFData (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: ModuleG mname -> () #

type Rep (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep (ModuleG mname) = D1 ('MetaData "ModuleG" "Cryptol.TypeCheck.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 mname) :*: (S1 ('MetaSel ('Just "mDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Text]) :*: S1 ('MetaSel ('Just "mExports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExportSpec Name)))) :*: ((S1 ('MetaSel ('Just "mParamTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam)) :*: S1 ('MetaSel ('Just "mParamFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam))) :*: (S1 ('MetaSel ('Just "mParamConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :*: S1 ('MetaSel ('Just "mParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctorParams)))) :*: (((S1 ('MetaSel ('Just "mFunctors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name (ModuleG Name))) :*: S1 ('MetaSel ('Just "mNested") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Set Name))) :*: (S1 ('MetaSel ('Just "mTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: S1 ('MetaSel ('Just "mNominalTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name NominalType)))) :*: ((S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]) :*: S1 ('MetaSel ('Just "mSubmodules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name Submodule))) :*: (S1 ('MetaSel ('Just "mSignatures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name ModParamNames)) :*: S1 ('MetaSel ('Just "mInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv))))))

data Decl Source #

Constructors

Decl 

Instances

Instances details
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 #

Show Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Decl -> ShowS #

show :: Decl -> String #

showList :: [Decl] -> ShowS #

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 #

TraverseNames Decl Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Decl -> f Decl Source #

ModuleInstance Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

ShowParseable Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Decl -> Decl Source #

PP Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Decl -> Doc Source #

NFData Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Decl -> () #

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

data CaseAlt Source #

Used for case expressions. Similar to a lambda, the variables are bound by the value examined in the case.

Constructors

CaseAlt [(Name, Type)] Expr 

Instances

Instances details
Generic CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep CaseAlt :: Type -> Type #

Methods

from :: CaseAlt -> Rep CaseAlt x #

to :: Rep CaseAlt x -> CaseAlt #

Show CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

FreeVars CaseAlt Source # 
Instance details

Defined in Cryptol.IR.FreeVars

TraverseNames CaseAlt Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => CaseAlt -> f CaseAlt Source #

ShowParseable CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

PP CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> CaseAlt -> Doc Source #

NFData CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: CaseAlt -> () #

type Rep CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep CaseAlt = D1 ('MetaData "CaseAlt" "Cryptol.TypeCheck.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "CaseAlt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Type)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))

data DocFor Source #

Instances

Instances details
PP DocFor Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> DocFor -> Doc Source #

data TCTopEntity Source #

Instances

Instances details
Generic TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep TCTopEntity :: Type -> Type #

Show TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

TVars TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

PP TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> TCTopEntity -> Doc Source #

NFData TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: TCTopEntity -> () #

PP (WithNames TCTopEntity) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

data DeclGroup Source #

Constructors

Recursive [Decl]

Mutually recursive declarations

NonRecursive Decl

Non-recursive declaration

Instances

Instances details
Generic DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep DeclGroup :: Type -> Type #

Show DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

TraverseNames DeclGroup Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => DeclGroup -> f DeclGroup Source #

ModuleInstance DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

ShowParseable DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

PP DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> DeclGroup -> Doc Source #

NFData DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclGroup -> () #

PP (WithNames DeclGroup) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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 Submodule Source #

Constructors

Submodule 

Instances

Instances details
Generic Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Submodule :: Type -> Type #

Show Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

ModuleInstance Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

NFData Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Submodule -> () #

type Rep Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Submodule = D1 ('MetaData "Submodule" "Cryptol.TypeCheck.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "Submodule" 'PrefixI 'True) (S1 ('MetaSel ('Just "smIface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IfaceNames Name)) :*: S1 ('MetaSel ('Just "smInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv)))

data DeclDef Source #

Constructors

DPrim 
DForeign FFIFunType (Maybe Expr)

Foreign functions can have an optional cryptol implementation

DExpr Expr 

Instances

Instances details
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 #

Show DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

FreeVars DeclDef Source # 
Instance details

Defined in Cryptol.IR.FreeVars

TraverseNames DeclDef Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => DeclDef -> f DeclDef Source #

ShowParseable DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

TVars DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

NFData DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclDef -> () #

PP (WithNames DeclDef) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

data DocItem Source #

Constructors

DocItem 

Fields

findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)] Source #

Find all the foreign declarations in the module and return their names and FFIFunTypes.

tcTopEntityToModule :: TCTopEntity -> Module Source #

Panics if the entity is not a module

emptyModule :: mname -> ModuleG mname Source #

findForeignDeclsInFunctors :: ModuleG mname -> [Name] Source #

Find all the foreign declarations that are in functors, including in the top-level module itself if it is a functor. This is used to report an error

isParametrizedModule :: ModuleG mname -> Bool Source #

Is this a parameterized module?

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

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

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

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

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

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

dropLocs :: Expr -> Expr Source #

Remove outermost locations

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

Show Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

TraverseNames Name Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Name -> f Name Source #

ModuleInstance Name Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

ShowParseable Name Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

ppPrec :: Int -> Name -> Doc Source #

PPName Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

NFData Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: Name -> () #

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 #

type Rep Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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 "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] #

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 #

Show TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TFun -> ShowS #

show :: TFun -> String #

showList :: [TFun] -> ShowS #

HasKind TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind Source #

PP TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TFun -> Doc Source #

NFData TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: 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 #

type Rep TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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
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 #

Show Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

ShowParseable Selector Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

ppPrec :: Int -> Selector -> Doc Source #

NFData Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

rnf :: Selector -> () #

Eq Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Ord Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

data ImportG mname Source #

An import declaration.

Constructors

Import 

Fields

Instances

Instances details
Generic (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImportG mname) :: Type -> Type #

Methods

from :: ImportG mname -> Rep (ImportG mname) x #

to :: Rep (ImportG mname) x -> ImportG mname #

Show mname => Show (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImportG mname -> ShowS #

show :: ImportG mname -> String #

showList :: [ImportG mname] -> ShowS #

PP mname => PP (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportG mname -> Doc Source #

NFData mname => NFData (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportG mname -> () #

type Rep (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

data ImpName name Source #

The name of an imported module

Constructors

ImpTop ModName

A top-level module

ImpNested name

The module in scope with the given name

Instances

Instances details
Rename ImpName Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImpName name) :: Type -> Type #

Methods

from :: ImpName name -> Rep (ImpName name) x #

to :: Rep (ImpName name) x -> ImpName name #

Show name => Show (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImpName name -> ShowS #

show :: ImpName name -> String #

showList :: [ImpName name] -> ShowS #

ModuleInstance name => ModuleInstance (ImpName name) Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: ImpName name -> ImpName name Source #

PP name => PP (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImpName name -> Doc Source #

NFData name => NFData (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImpName name -> () #

Eq name => Eq (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: ImpName name -> ImpName name -> Bool #

(/=) :: ImpName name -> ImpName name -> Bool #

Ord name => Ord (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ImpName name -> ImpName name -> Ordering #

(<) :: ImpName name -> ImpName name -> Bool #

(<=) :: ImpName name -> ImpName name -> Bool #

(>) :: ImpName name -> ImpName name -> Bool #

(>=) :: ImpName name -> ImpName name -> Bool #

max :: ImpName name -> ImpName name -> ImpName name #

min :: ImpName name -> ImpName name -> ImpName name #

type Rep (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ImpName name) = D1 ('MetaData "ImpName" "Cryptol.Parser.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "ImpTop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName)) :+: C1 ('MetaCons "ImpNested" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name)))

data ImportSpec Source #

The list of names following an import.

Constructors

Hiding [Ident] 
Only [Ident] 

Instances

Instances details
Generic ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ImportSpec :: Type -> Type #

Show ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

PP ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportSpec -> Doc Source #

NFData ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportSpec -> () #

Eq ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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
Generic ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ExportType :: Type -> Type #

Show ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ExportType -> () #

Eq ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Ord ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type))

newtype ExportSpec name Source #

Constructors

ExportSpec (Map Namespace (Set name)) 

Instances

Instances details
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 #

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 #

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 #

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 #

(Ord a, TraverseNames a) => TraverseNames (ExportSpec a) Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ExportSpec a -> f (ExportSpec a) Source #

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-3.2.0-35bDsq0QUVdvBXha47jji" 'True) (C1 ('MetaCons "ExportSpec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Namespace (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.

isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool Source #

data Pragma Source #

Instances

Instances details
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 #

Show Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma Source #

PP Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pragma -> Doc Source #

NFData Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Pragma -> () #

Eq Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: Pragma -> Pragma -> Bool #

(/=) :: Pragma -> Pragma -> Bool #

type Rep Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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
Generic Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Associated Types

type Rep Fixity :: Type -> Type #

Methods

from :: Fixity -> Rep Fixity x #

to :: Rep Fixity x -> Fixity #

Show Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

PP Fixity Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Fixity -> Doc Source #

NFData Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Fixity -> () #

Eq Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

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

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

Ord Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" '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.

Instances

Instances details
Semigroup PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

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 #

Show PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

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-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "PrimMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "primDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name)) :*: S1 ('MetaSel ('Just "primTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name))))

data DocFor Source #

Instances

Instances details
PP DocFor Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> DocFor -> Doc Source #