Cryptol.TypeCheck.AST

Documentation

data DeclDef

Constructors

DPrim

DExpr Expr

Instances

Show DeclDef

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> DeclDef -> ShowS

show :: DeclDef -> String

showList :: [DeclDef] -> ShowS

Generic DeclDef

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclDef -> ()

ShowParseable DeclDef

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: DeclDef -> Doc

FreeVars DeclDef

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: DeclDef -> Deps

TVars DeclDef

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclDef -> DeclDef

PP (WithNames DeclDef)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames DeclDef -> Doc

type Rep DeclDef

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef = D1 (MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Decl

Fields

• dName :: !Name
• dSignature :: Schema
• dDefinition :: DeclDef
• dPragmas :: [Pragma]
• dInfix :: !Bool
• dFixity :: Maybe Fixity
• dDoc :: Maybe String

Instances

Show Decl

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Decl -> ShowS

show :: Decl -> String

showList :: [Decl] -> ShowS

Generic Decl

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Decl -> ()

PP Decl

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Decl -> Doc

ShowParseable Decl

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Decl -> Doc

Defs Decl

Defined in Cryptol.IR.FreeVars

Methods

defs :: Decl -> Set Name

FreeVars Decl

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Decl -> Deps

TVars Decl

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Decl -> Decl

PP (WithNames Decl)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames Decl -> Doc

type Rep Decl

Defined in Cryptol.TypeCheck.AST

type Rep Decl = D1 (MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Recursive [Decl]

Mutually recursive declarations

NonRecursive Decl

Non-recursive declaration

Instances

Show DeclGroup

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> DeclGroup -> ShowS

show :: DeclGroup -> String

showList :: [DeclGroup] -> ShowS

Generic DeclGroup

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclGroup -> ()

PP DeclGroup

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> DeclGroup -> Doc

ShowParseable DeclGroup

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: DeclGroup -> Doc

Defs DeclGroup

Defined in Cryptol.IR.FreeVars

Methods

defs :: DeclGroup -> Set Name

FreeVars DeclGroup

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: DeclGroup -> Deps

TVars DeclGroup

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclGroup -> DeclGroup

PP (WithNames DeclGroup)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames DeclGroup -> Doc

type Rep DeclGroup

Defined in Cryptol.TypeCheck.AST

type Rep DeclGroup = D1 (MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

From Name Type Type Expr

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

Let Decl

Instances

Show Match

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Match -> ShowS

show :: Match -> String

showList :: [Match] -> ShowS

Generic Match

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Match -> ()

PP Match

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Match -> Doc

ShowParseable Match

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Match -> Doc

Defs Match

Defined in Cryptol.IR.FreeVars

Methods

defs :: Match -> Set Name

FreeVars Match

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Match -> Deps

TVars Match

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Match -> Match

PP (WithNames Match)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames Match -> Doc

type Rep Match

Defined in Cryptol.TypeCheck.AST

type Rep Match = D1 (MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Show Expr

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Generic Expr

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Expr -> ()

PP Expr

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Expr -> Doc

ShowParseable Expr

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Expr -> Doc

FreeVars Expr

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Expr -> Deps

TVars Expr

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Expr -> Expr

PP (WithNames Expr)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames Expr -> Doc

type Rep Expr

Defined in Cryptol.TypeCheck.AST

type Rep Expr = D1 (MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

A value parameter of a module.

Constructors

ModVParam

Fields

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

Instances

Show ModVParam

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> ModVParam -> ShowS

show :: ModVParam -> String

showList :: [ModVParam] -> ShowS

Generic ModVParam

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: ModVParam -> ()

type Rep ModVParam

Defined in Cryptol.TypeCheck.AST

type Rep ModVParam = D1 (MetaData "ModVParam" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Show ModTParam

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> ModTParam -> ShowS

show :: ModTParam -> String

showList :: [ModTParam] -> ShowS

Generic ModTParam

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: ModTParam -> ()

type Rep ModTParam

Defined in Cryptol.TypeCheck.AST

type Rep ModTParam = D1 (MetaData "ModTParam" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

A Cryptol module.

Constructors

Module

Fields

• mName :: !ModName
• mExports :: ExportSpec Name
• mImports :: [Import]
• mTySyns :: Map Name TySyn

  This is just the type-level type synonyms of a module.

• mNewtypes :: Map Name Newtype
• mParamTypes :: Map Name ModTParam
• mParamConstraints :: [Located Prop]
• mParamFuns :: Map Name ModVParam
• mDecls :: [DeclGroup]

Instances

Show Module

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

Generic Module

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Module -> ()

PP Module

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> Module -> Doc

TVars Module

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Module -> Module

PP (WithNames Module)

Defined in Cryptol.TypeCheck.AST

Methods

ppPrec :: Int -> WithNames Module -> Doc

type Rep Module

Defined in Cryptol.TypeCheck.AST

type Rep Module = D1 (MetaData "Module" "Cryptol.TypeCheck.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 "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

Is this a parameterized module?

mtpParam :: ModTParam -> TParam

groupDecls :: DeclGroup -> [Decl]

ePrim :: PrimMap -> Ident -> Expr

Construct a primitive, given a map to the unique names of the Cryptol module.

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

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

eString :: PrimMap -> String -> Expr

eChar :: PrimMap -> Char -> Expr

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

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

splitAbs :: Expr -> Maybe ((Name, Type), Expr)

splitTAbs :: Expr -> Maybe (TParam, Expr)

splitProofAbs :: Expr -> Maybe (Prop, Expr)

splitTApp :: Expr -> Maybe (Type, Expr)

splitProofApp :: Expr -> Maybe ((), Expr)

splitExprInst :: Expr -> (Expr, [Type], Int)

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

Instances

Eq Name

Defined in Cryptol.ModuleSystem.Name

Methods

(==) :: Name -> Name -> Bool

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

Ord Name

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

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Generic Name

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: Name -> ()

PPName Name

Defined in Cryptol.ModuleSystem.Name

Methods

ppNameFixity :: Name -> Maybe (Assoc, Int)

ppPrefixName :: Name -> Doc

ppInfixName :: Name -> Doc

PP Name

Defined in Cryptol.ModuleSystem.Name

Methods

ppPrec :: Int -> Name -> Doc

ShowParseable Name

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Name -> Doc

FromDecl (Decl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: Decl Name -> Maybe (Bind Name)

toParamFun :: Decl Name -> Maybe (ParameterFun Name)

toParamConstraints :: Decl Name -> [Located (Prop Name)]

toTyDecl :: Decl Name -> Maybe TyDecl

isTopDecl :: Decl Name -> Bool

FromDecl (TopDecl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: TopDecl Name -> Maybe (Bind Name)

toParamFun :: TopDecl Name -> Maybe (ParameterFun Name)

toParamConstraints :: TopDecl Name -> [Located (Prop Name)]

toTyDecl :: TopDecl Name -> Maybe TyDecl

isTopDecl :: TopDecl Name -> Bool

type Rep Name

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 (MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Bounded TFun

Defined in Cryptol.Prims.Syntax

Methods

minBound :: TFun

maxBound :: TFun

Enum TFun

Defined in Cryptol.Prims.Syntax

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

Defined in Cryptol.Prims.Syntax

Methods

(==) :: TFun -> TFun -> Bool

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

Ord TFun

Defined in Cryptol.Prims.Syntax

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

Defined in Cryptol.Prims.Syntax

Methods

showsPrec :: Int -> TFun -> ShowS

show :: TFun -> String

showList :: [TFun] -> ShowS

Generic TFun

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TFun :: Type -> Type

Methods

from :: TFun -> Rep TFun x

to :: Rep TFun x -> TFun

NFData TFun

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TFun -> ()

PPName TFun

Defined in Cryptol.Prims.Syntax

Methods

ppNameFixity :: TFun -> Maybe (Assoc, Int)

ppPrefixName :: TFun -> Doc

ppInfixName :: TFun -> Doc

PP TFun

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TFun -> Doc

HasKind TFun

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: TFun -> Kind

type Rep TFun

Defined in Cryptol.Prims.Syntax

type Rep TFun = D1 (MetaData "TFun" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Selectors are used for projecting from various components. Each selector has an option spec to specify the shape of the thing that is being selected. Currently, there is no surface syntax for list selectors, but they are used during the desugaring of patterns.

Constructors

TupleSel Int (Maybe Int)

Zero-based tuple selection. Optionally specifies the shape of the tuple (one-based).

RecordSel Ident (Maybe [Ident])

Record selection. Optionally specifies the shape of the record.

ListSel Int (Maybe Int)

List selection. Optionally specifies the length of the list.

Instances

Eq Selector

Defined in Cryptol.Parser.Selector

Methods

(==) :: Selector -> Selector -> Bool

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

Ord Selector

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

Defined in Cryptol.Parser.Selector

Methods

showsPrec :: Int -> Selector -> ShowS

show :: Selector -> String

showList :: [Selector] -> ShowS

Generic Selector

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

Defined in Cryptol.Parser.Selector

Methods

rnf :: Selector -> ()

PP Selector

Defined in Cryptol.Parser.Selector

Methods

ppPrec :: Int -> Selector -> Doc

ShowParseable Selector

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Selector -> Doc

type Rep Selector

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 (MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

An import declaration.

Constructors

Import

Fields

• iModule :: !ModName
• iAs :: Maybe ModName
• iSpec :: Maybe ImportSpec

Instances

Eq Import

Defined in Cryptol.Parser.AST

Methods

(==) :: Import -> Import -> Bool

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

Show Import

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Import -> ShowS

show :: Import -> String

showList :: [Import] -> ShowS

Generic Import

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Import -> ()

PP Import

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Import -> Doc

type Rep Import

Defined in Cryptol.Parser.AST

type Rep Import = D1 (MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Eq ImportSpec

Defined in Cryptol.Parser.AST

Methods

(==) :: ImportSpec -> ImportSpec -> Bool

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

Show ImportSpec

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImportSpec -> ShowS

show :: ImportSpec -> String

showList :: [ImportSpec] -> ShowS

Generic ImportSpec

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportSpec -> ()

PP ImportSpec

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportSpec -> Doc

type Rep ImportSpec

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 (MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Export information for a declaration.

Constructors

Public

Private

Instances

Eq ExportType

Defined in Cryptol.Parser.AST

Methods

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

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

Ord ExportType

Defined in Cryptol.Parser.AST

Methods

compare :: ExportType -> ExportType -> Ordering

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

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

(>) :: ExportType -> ExportType -> Bool

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

max :: ExportType -> ExportType -> ExportType

min :: ExportType -> ExportType -> ExportType

Show ExportType

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ExportType -> ShowS

show :: ExportType -> String

showList :: [ExportType] -> ShowS

Generic ExportType

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ExportType -> ()

type Rep ExportType

Defined in Cryptol.Parser.AST

type Rep ExportType = D1 (MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "Public" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Private" PrefixI False) (U1 :: Type -> Type))

data ExportSpec name

Constructors

ExportSpec

Fields

• eTypes :: Set name
• eBinds :: Set name

Instances

Show name => Show (ExportSpec name)

Defined in Cryptol.ModuleSystem.Exports

Methods

showsPrec :: Int -> ExportSpec name -> ShowS

show :: ExportSpec name -> String

showList :: [ExportSpec name] -> ShowS

Generic (ExportSpec name)

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)

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)

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)

Defined in Cryptol.ModuleSystem.Exports

Methods

rnf :: ExportSpec name -> ()

type Rep (ExportSpec name)

Defined in Cryptol.ModuleSystem.Exports

type Rep (ExportSpec name) = D1 (MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Check to see if a binding is exported.

isExportedType :: Ord name => name -> ExportSpec name -> Bool

Check to see if a type synonym is exported.

data Pragma

Constructors

PragmaNote String

PragmaProperty

Instances

Eq Pragma

Defined in Cryptol.Parser.AST

Methods

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

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

Show Pragma

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Generic Pragma

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Pragma -> ()

PP Pragma

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pragma -> Doc

NoPos Pragma

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma

type Rep Pragma

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 (MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Fixity

Fields

• fAssoc :: !Assoc
• fLevel :: !Int

Instances

Eq Fixity

Defined in Cryptol.Parser.Fixity

Methods

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

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

Show Fixity

Defined in Cryptol.Parser.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

Generic Fixity

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

Defined in Cryptol.Parser.Fixity

Methods

rnf :: Fixity -> ()

type Rep Fixity

Defined in Cryptol.Parser.Fixity

type Rep Fixity = D1 (MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Constructors

PrimMap

Fields

• primDecls :: Map Ident Name
• primTypes :: Map Ident Name

Instances

Show PrimMap

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> PrimMap -> ShowS

show :: PrimMap -> String

showList :: [PrimMap] -> ShowS

Generic PrimMap

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: PrimMap -> ()

type Rep PrimMap

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 (MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

TCErrorMessage

Fields

• tcErrorMessage :: !String

Instances

Eq TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

compare :: TCErrorMessage -> TCErrorMessage -> Ordering

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

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

(>) :: TCErrorMessage -> TCErrorMessage -> Bool

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

max :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage

min :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage

Show TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

showsPrec :: Int -> TCErrorMessage -> ShowS

show :: TCErrorMessage -> String

showList :: [TCErrorMessage] -> ShowS

Generic TCErrorMessage

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TCErrorMessage :: Type -> Type

Methods

from :: TCErrorMessage -> Rep TCErrorMessage x

to :: Rep TCErrorMessage x -> TCErrorMessage

NFData TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TCErrorMessage -> ()

PP TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TCErrorMessage -> Doc

type Rep TCErrorMessage

Defined in Cryptol.Prims.Syntax

type Rep TCErrorMessage = D1 (MetaData "TCErrorMessage" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "TCErrorMessage" PrefixI True) (S1 (MetaSel (Just "tcErrorMessage") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 String)))

module Cryptol.TypeCheck.Type