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

TVars DeclDef

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclDef -> DeclDef

ShowParseable DeclDef

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: DeclDef -> Doc

FreeVars DeclDef

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: DeclDef -> Deps

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

Constructors

Decl

Fields

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

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

TVars Decl

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Decl -> Decl

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

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

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

TVars DeclGroup

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclGroup -> DeclGroup

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

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

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

TVars Match

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Match -> Match

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

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

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

TVars Expr

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Expr -> Expr

ShowParseable Expr

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Expr -> Doc

FreeVars Expr

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Expr -> Deps

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

A value parameter of a module.

Constructors

ModVParam

Fields

• mvpName :: Name
• mvpType :: Schema
• mvpDoc :: Maybe Text
• 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.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

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 Text

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

A Cryptol module.

Constructors

Module

Fields

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

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

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

Instances

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: S1 ('MetaSel ('Just "mExports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExportSpec Name))) :*: (S1 ('MetaSel ('Just "mImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Import]) :*: (S1 ('MetaSel ('Just "mTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: S1 ('MetaSel ('Just "mNewtypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name Newtype))))) :*: ((S1 ('MetaSel ('Just "mPrimTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name AbstractType)) :*: S1 ('MetaSel ('Just "mParamTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam))) :*: (S1 ('MetaSel ('Just "mParamConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :*: (S1 ('MetaSel ('Just "mParamFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam)) :*: S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]))))))

isParametrizedModule :: Module -> Bool

Is this a parameterized module?

mtpParam :: ModTParam -> TParam

groupDecls :: DeclGroup -> [Decl]

ePrim :: PrimMap -> PrimIdent -> Expr

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

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 Fixity

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

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

Methods

minBound :: TFun

maxBound :: TFun

Enum TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TFun -> ShowS

show :: TFun -> String

showList :: [TFun] -> ShowS

Generic TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TFun -> ()

PP TFun

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TFun -> Doc

HasKind TFun

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind

type Rep TFun

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

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

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

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

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

Constructors

Fixity

Fields

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

Instances

Eq Fixity

Defined in Cryptol.Utils.Fixity

Methods

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

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

Show Fixity

Defined in Cryptol.Utils.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

Generic Fixity

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

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Fixity -> ()

PP Fixity

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Fixity -> Doc

type Rep Fixity

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

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

Constructors

PrimMap

Fields

• primDecls :: Map PrimIdent Name
• primTypes :: Map PrimIdent 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

Semigroup PrimMap

Defined in Cryptol.ModuleSystem.Name

Methods

(<>) :: PrimMap -> PrimMap -> PrimMap

sconcat :: NonEmpty PrimMap -> PrimMap

stimes :: Integral b => b -> PrimMap -> 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.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))))

module Cryptol.TypeCheck.Type