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

Generic DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep DeclDef :: Type -> Type #

Methods

from :: DeclDef -> Rep DeclDef x #

to :: Rep DeclDef x -> DeclDef #

NFData DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclDef -> () #

TVars DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

ShowParseable DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

FreeVars DeclDef Source # 
Instance details

Defined in Cryptol.IR.FreeVars

PP (WithNames DeclDef) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 

Instances

Instances details
Show Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Decl -> ShowS #

show :: Decl -> String #

showList :: [Decl] -> ShowS #

Generic Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Decl :: Type -> Type #

Methods

from :: Decl -> Rep Decl x #

to :: Rep Decl x -> Decl #

NFData Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Decl -> () #

PP Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

TVars Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

ShowParseable Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Defs Decl Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

defs :: Decl -> Set Name Source #

FreeVars Decl Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Decl -> Deps Source #

PP (WithNames Decl) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

type Rep Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

Generic DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep DeclGroup :: Type -> Type #

NFData DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclGroup -> () #

PP DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

TVars DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

ShowParseable DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

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

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-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "Recursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Decl])) :+: C1 ('MetaCons "NonRecursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Decl)))

data Match Source #

Constructors

From Name Type Type Expr

Type arguments are the length and element type of the sequence expression

Let Decl 

Instances

Instances details
Show Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Match -> ShowS #

show :: Match -> String #

showList :: [Match] -> ShowS #

Generic Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Match :: Type -> Type #

Methods

from :: Match -> Rep Match x #

to :: Rep Match x -> Match #

NFData Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Match -> () #

PP Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

TVars Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

ShowParseable Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Defs Match Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

defs :: Match -> Set Name Source #

FreeVars Match Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Match -> Deps Source #

PP (WithNames Match) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

type Rep Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

data Expr Source #

Constructors

EList [Expr] Type

List value (with type of elements)

ETuple [Expr]

Tuple value

ERec (RecordMap Ident Expr)

Record value

ESel Expr Selector

Elimination for tuplerecordlist

ESet Type Expr Selector Expr

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

EIf Expr Expr Expr

If-then-else

EComp Type Type Expr [[Match]]

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

EVar Name

Use of a bound variable

ETAbs TParam Expr

Function Value

ETApp Expr Type

Type application

EApp Expr Expr

Function application

EAbs Name Type Expr

Function value

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 #

TVars Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

ShowParseable Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

FreeVars Expr Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Expr -> Deps Source #

PP (WithNames Expr) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

type Rep Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (((C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr])) :+: C1 ('MetaCons "ERec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Expr))))) :+: ((C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)) :+: C1 ('MetaCons "ESet" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "EComp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match]])))))) :+: (((C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "EAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "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 

Instances

Instances details
Show ModVParam Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Generic ModVParam Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep ModVParam :: Type -> Type #

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "ModVParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mvpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "mvpType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema)) :*: (S1 ('MetaSel ('Just "mvpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "mvpFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)))))

data ModTParam Source #

A type parameter of a module.

Constructors

ModTParam 

Fields

Instances

Instances details
Show ModTParam Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Generic ModTParam Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep ModTParam :: Type -> Type #

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "ModTParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mtpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "mtpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Just "mtpNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "mtpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)))))

data Module Source #

A Cryptol module.

Constructors

Module 

Instances

Instances details
Show Module Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

type Rep Module Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

isParametrizedModule :: Module -> 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.

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

splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) 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

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Ord Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Show Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

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

type Rep Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

data Import Source #

An import declaration.

Constructors

Import 

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

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Show ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Generic ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ImportSpec :: Type -> Type #

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Ord ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Show ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Generic ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ExportType :: Type -> Type #

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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.Utils.Fixity

Methods

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

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

Show Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Generic Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Associated Types

type Rep Fixity :: Type -> Type #

Methods

from :: Fixity -> Rep Fixity x #

to :: Rep Fixity x -> Fixity #

NFData Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Fixity -> () #

PP Fixity Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

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

type Rep Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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
Show 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 #

Semigroup 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-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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))))