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

type Module = ModuleG ModName Source #

data ModuleG mname Source #

A Cryptol module.

Constructors

Module 

Fields

Instances

Instances details
Generic (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep (ModuleG mname) 
Instance details

Defined in Cryptol.TypeCheck.AST

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

Methods

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

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

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

Defined in Cryptol.TypeCheck.AST

Methods

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

show :: ModuleG mname -> String #

showList :: [ModuleG mname] -> ShowS #

ModuleInstance (ModuleG name) Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: ModuleG name -> ModuleG name Source #

TVars (ModuleG names) Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

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

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ModuleG n -> Doc Source #

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

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames (ModuleG n) -> Doc Source #

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

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: ModuleG mname -> () #

type Rep (ModuleG mname) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

data Match Source #

Constructors

From Name Type Type Expr

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

Let Decl 

Instances

Instances details
Generic Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Match 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Match = D1 ('MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

Methods

from :: Match -> Rep Match x #

to :: Rep Match x -> Match #

Show Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Match -> ShowS #

show :: Match -> String #

showList :: [Match] -> ShowS #

Defs Match Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

defs :: Match -> Set Name Source #

FreeVars Match Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Match -> Deps Source #

TraverseNames Match Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ShowParseable Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Match -> Doc Void Source #

TVars Match Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

PP Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Match -> Doc Source #

NFData Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Match -> () #

PP (WithNames Match) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames Match -> Doc Source #

type Rep Match Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Match = D1 ('MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "From" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Decl)))

data Expr Source #

Constructors

EList [Expr] Type

List value (with type of elements)

ETuple [Expr]

Tuple value

ERec (RecordMap Ident Expr)

Record value

ESel Expr Selector

Elimination for tuplerecordlist

ESet Type Expr Selector Expr

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

EIf Expr Expr Expr

If-then-else

ECase Expr (Map Ident CaseAlt) (Maybe CaseAlt)

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

EComp Type Type Expr [[Match]]

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

EVar Name

Use of a bound variable

ETAbs TParam Expr

Function Value

ETApp Expr Type

Type application

EApp Expr Expr

Function application

EAbs Name Type Expr

Function value

ELocated Range Expr

Source location information

EProofAbs Prop Expr

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

EProofApp Expr

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

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

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

Use ePropGuards when constructing to get automatic simplification of trivial constraints

Instances

Instances details
Generic Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Expr 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((((C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: (C1 ('MetaCons "ERec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Expr))) :+: C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)))) :+: ((C1 ('MetaCons "ESet" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ECase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident CaseAlt)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe CaseAlt)))) :+: (C1 ('MetaCons "EComp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match]]))) :+: C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "ELocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EProofAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "EProofApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: (C1 ('MetaCons "EWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup])) :+: C1 ('MetaCons "EPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [([Prop], Expr)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))))

Methods

from :: Expr -> Rep Expr x #

to :: Rep Expr x -> Expr #

Show Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

FreeVars Expr Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Expr -> Deps Source #

TraverseNames Expr Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

HasLoc Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

getLoc :: Expr -> Maybe Range Source #

ShowParseable Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Expr -> Doc Void Source #

TVars Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

PP Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Expr -> Doc Source #

NFData Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Expr -> () #

PP (WithNames Expr) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames Expr -> Doc Source #

type Rep Expr Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((((C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: (C1 ('MetaCons "ERec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Expr))) :+: C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)))) :+: ((C1 ('MetaCons "ESet" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ECase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident CaseAlt)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe CaseAlt)))) :+: (C1 ('MetaCons "EComp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match]]))) :+: C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "ELocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EProofAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "EProofApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: (C1 ('MetaCons "EWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup])) :+: C1 ('MetaCons "EPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [([Prop], Expr)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))))

data Decl Source #

Constructors

Decl 

Fields

Instances

Instances details
Generic Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Decl 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Decl = D1 ('MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

Methods

from :: Decl -> Rep Decl x #

to :: Rep Decl x -> Decl #

Show Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Decl -> ShowS #

show :: Decl -> String #

showList :: [Decl] -> ShowS #

Defs Decl Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

defs :: Decl -> Set Name Source #

FreeVars Decl Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Decl -> Deps Source #

TraverseNames Decl Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ModuleInstance Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: Decl -> Decl Source #

ShowParseable Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Decl -> Doc Void Source #

TVars Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

PP Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Decl -> Doc Source #

NFData Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Decl -> () #

PP (WithNames Decl) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames Decl -> Doc Source #

type Rep Decl Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Decl = D1 ('MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 CaseAlt Source #

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

Constructors

CaseAlt [(Name, Type)] Expr 

Instances

Instances details
Generic CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep CaseAlt 
Instance details

Defined in Cryptol.TypeCheck.AST

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

Methods

from :: CaseAlt -> Rep CaseAlt x #

to :: Rep CaseAlt x -> CaseAlt #

Show CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> CaseAlt -> ShowS #

show :: CaseAlt -> String #

showList :: [CaseAlt] -> ShowS #

FreeVars CaseAlt Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: CaseAlt -> Deps Source #

TraverseNames CaseAlt Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ShowParseable CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: CaseAlt -> Doc Void Source #

TVars CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> CaseAlt -> CaseAlt Source #

PP CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> CaseAlt -> Doc Source #

NFData CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: CaseAlt -> () #

type Rep CaseAlt Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

data FFI Source #

Constructors

CallC (FFIFunType FFIType) 
CallAbstract (FFIFunType Type) 

Instances

Instances details
Generic FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep FFI 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep FFI = D1 ('MetaData "FFI" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "CallC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType FFIType))) :+: C1 ('MetaCons "CallAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType Type))))

Methods

from :: FFI -> Rep FFI x #

to :: Rep FFI x -> FFI #

Show FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> FFI -> ShowS #

show :: FFI -> String #

showList :: [FFI] -> ShowS #

FreeVars FFI Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: FFI -> Deps Source #

TraverseNames FFI Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ShowParseable FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: FFI -> Doc Void Source #

NFData FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: FFI -> () #

type Rep FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep FFI = D1 ('MetaData "FFI" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "CallC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType FFIType))) :+: C1 ('MetaCons "CallAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType Type))))

data Submodule Source #

Constructors

Submodule 

Fields

Instances

Instances details
Generic Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep Submodule 
Instance details

Defined in Cryptol.TypeCheck.AST

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

Methods

from :: Submodule -> Rep Submodule x #

to :: Rep Submodule x -> Submodule #

Show Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> Submodule -> ShowS #

show :: Submodule -> String #

showList :: [Submodule] -> ShowS #

ModuleInstance Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: Submodule -> Submodule Source #

NFData Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: Submodule -> () #

type Rep Submodule Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

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

groupDecls :: DeclGroup -> [Decl] Source #

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

data DeclGroup Source #

Constructors

Recursive [Decl]

Mutually recursive declarations

NonRecursive Decl

Non-recursive declaration

Instances

Instances details
Generic DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep DeclGroup 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

Methods

from :: DeclGroup -> Rep DeclGroup x #

to :: Rep DeclGroup x -> DeclGroup #

Show DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> DeclGroup -> ShowS #

show :: DeclGroup -> String #

showList :: [DeclGroup] -> ShowS #

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

Methods

freeVars :: DeclGroup -> Deps Source #

TraverseNames DeclGroup Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ModuleInstance DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: DeclGroup -> DeclGroup Source #

ShowParseable DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: DeclGroup -> Doc Void Source #

TVars DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclGroup -> DeclGroup Source #

PP DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> DeclGroup -> Doc Source #

NFData DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclGroup -> () #

PP (WithNames DeclGroup) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames DeclGroup -> Doc Source #

type Rep DeclGroup Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

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

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

splitApp :: Expr -> Maybe (Expr, Expr) Source #

data DeclDef Source #

Constructors

DPrim 
DForeign FFI (Maybe Expr)

Foreign functions can have an optional cryptol implementation

DExpr Expr 

Instances

Instances details
Generic DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep DeclDef 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DForeign" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFI) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

Methods

from :: DeclDef -> Rep DeclDef x #

to :: Rep DeclDef x -> DeclDef #

Show DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> DeclDef -> ShowS #

show :: DeclDef -> String #

showList :: [DeclDef] -> ShowS #

FreeVars DeclDef Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: DeclDef -> Deps Source #

TraverseNames DeclDef Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ShowParseable DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: DeclDef -> Doc Void Source #

TVars DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclDef -> DeclDef Source #

NFData DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: DeclDef -> () #

PP (WithNames DeclDef) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames DeclDef -> Doc Source #

type Rep DeclDef Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DForeign" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFI) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

data TCTopEntity Source #

Constructors

TCTopModule (ModuleG ModName) 
TCTopSignature ModName ModParamNames 

Instances

Instances details
Generic TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep TCTopEntity 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep TCTopEntity = D1 ('MetaData "TCTopEntity" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "TCTopModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleG ModName))) :+: C1 ('MetaCons "TCTopSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModParamNames)))

Methods

from :: TCTopEntity -> Rep TCTopEntity x #

to :: Rep TCTopEntity x -> TCTopEntity #

Show TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> TCTopEntity -> ShowS #

show :: TCTopEntity -> String #

showList :: [TCTopEntity] -> ShowS #

TVars TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> TCTopEntity -> TCTopEntity Source #

PP TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> TCTopEntity -> Doc Source #

NFData TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: TCTopEntity -> () #

PP (WithNames TCTopEntity) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames TCTopEntity -> Doc Source #

type Rep TCTopEntity Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep TCTopEntity = D1 ('MetaData "TCTopEntity" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "TCTopModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleG ModName))) :+: C1 ('MetaCons "TCTopSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModParamNames)))

tcTopEntitytName :: TCTopEntity -> ModName Source #

tcTopEntityToModule :: TCTopEntity -> Module Source #

Panics if the entity is not a module

emptyModule :: mname -> ModuleG mname Source #

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

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

isParametrizedModule :: ModuleG mname -> Bool Source #

Is this a parameterized module?

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

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

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

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

eString :: PrimMap -> String -> Expr Source #

eChar :: PrimMap -> Char -> Expr Source #

eNumber :: PrimMap -> Integer -> Type -> Expr Source #

ePropGuards :: [([Prop], Expr)] -> Type -> Expr Source #

Construct a prop guard expression simplifying trivial cases.

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

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

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

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

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

splitLoc :: Expr -> Maybe (Range, Expr) Source #

dropLocs :: Expr -> Expr Source #

Remove outermost locations

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

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

Deconstruct an expression, typically polymorphic, into the types and proofs to which it is applied. Since we don't store the proofs, we just return the number of proof applications. The first type is the one closest to the expr.

data Name Source #

Instances

Instances details
Generic Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Associated Types

type Rep Name 
Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Name" 'PrefixI 'True) ((S1 ('MetaSel ('Just "nUnique") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "nInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NameInfo)) :*: (S1 ('MetaSel ('Just "nFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "nLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range))))

Methods

from :: Name -> Rep Name x #

to :: Rep Name x -> Name #

Show Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

TraverseNames Name Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ModuleInstance Name Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: Name -> Name Source #

ShowParseable Name Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Name -> Doc Void Source #

PP Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Name -> Doc Source #

PPName Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

ppNameFixity :: Name -> Maybe Fixity Source #

ppPrefixName :: Name -> Doc Source #

ppInfixName :: Name -> Doc Source #

NFData Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: Name -> () #

Eq Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

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

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

Ord Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

compare :: Name -> Name -> Ordering #

(<) :: Name -> Name -> Bool #

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

(>) :: Name -> Name -> Bool #

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

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

type Rep Name Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Name" 'PrefixI 'True) ((S1 ('MetaSel ('Just "nUnique") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "nInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NameInfo)) :*: (S1 ('MetaSel ('Just "nFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "nLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range))))

data TFun Source #

Built-in type functions. If you add additional user-visible constructors, please update primTys in Cryptol.Prims.Types.

Constructors

TCAdd
 : Num -> Num -> Num
TCSub
 : Num -> Num -> Num
TCMul
 : Num -> Num -> Num
TCDiv
 : Num -> Num -> Num
TCMod
 : Num -> Num -> Num
TCExp
 : Num -> Num -> Num
TCWidth
 : Num -> Num
TCMin
 : Num -> Num -> Num
TCMax
 : Num -> Num -> Num
TCCeilDiv
 : Num -> Num -> Num
TCCeilMod
 : Num -> Num -> Num
TCLenFromThenTo

: Num -> Num -> Num -> Num Example: [ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]

Instances

Instances details
Bounded TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

minBound :: TFun #

maxBound :: TFun #

Enum TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

succ :: TFun -> TFun #

pred :: TFun -> TFun #

toEnum :: Int -> TFun #

fromEnum :: TFun -> Int #

enumFrom :: TFun -> [TFun] #

enumFromThen :: TFun -> TFun -> [TFun] #

enumFromTo :: TFun -> TFun -> [TFun] #

enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] #

Generic TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TFun 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

Methods

from :: TFun -> Rep TFun x #

to :: Rep TFun x -> TFun #

Show TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TFun -> ShowS #

show :: TFun -> String #

showList :: [TFun] -> ShowS #

HasKind TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind Source #

PP TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> TFun -> Doc Source #

NFData TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TFun -> () #

Eq TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TFun -> TFun -> Ordering #

(<) :: TFun -> TFun -> Bool #

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

(>) :: TFun -> TFun -> Bool #

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

max :: TFun -> TFun -> TFun #

min :: TFun -> TFun -> TFun #

type Rep TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (((C1 ('MetaCons "TCAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMul" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCExp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TCWidth" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMax" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCCeilDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCCeilMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCLenFromThenTo" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Selector Source #

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

Constructors

TupleSel Int (Maybe Int)

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

RecordSel Ident (Maybe [Ident])

Record selection. Optionally specifies the shape of the record.

ListSel Int (Maybe Int)

List selection. Optionally specifies the length of the list.

Instances

Instances details
Generic Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Associated Types

type Rep Selector 
Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

Methods

from :: Selector -> Rep Selector x #

to :: Rep Selector x -> Selector #

Show Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

showsPrec :: Int -> Selector -> ShowS #

show :: Selector -> String #

showList :: [Selector] -> ShowS #

ShowParseable Selector Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Selector -> Doc Void Source #

PP Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Selector -> Doc Source #

NFData Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

rnf :: Selector -> () #

Eq Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

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

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

Ord Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

compare :: Selector -> Selector -> Ordering #

(<) :: Selector -> Selector -> Bool #

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

(>) :: Selector -> Selector -> Bool #

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

max :: Selector -> Selector -> Selector #

min :: Selector -> Selector -> Selector #

type Rep Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

type Import = ImportG ModName Source #

data ImportG mname Source #

An import declaration.

Constructors

Import 

Fields

Instances

Instances details
Generic (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImportG mname) 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) ((S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located mname)) :*: S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)) :*: (S1 ('MetaSel ('Just "iInst") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (ModuleInstanceArgs PName))) :*: S1 ('MetaSel ('Just "iDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text)))))))

Methods

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

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

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

Defined in Cryptol.Parser.AST

Methods

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

show :: ImportG mname -> String #

showList :: [ImportG mname] -> ShowS #

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

Defined in Cryptol.Parser.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ImportG mname -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportG mname -> () #

type Rep (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) ((S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Located mname)) :*: S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)) :*: (S1 ('MetaSel ('Just "iInst") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (ModuleInstanceArgs PName))) :*: S1 ('MetaSel ('Just "iDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text)))))))

data ImpName name Source #

The name of an imported module

Constructors

ImpTop ModName

A top-level module

ImpNested name

The module in scope with the given name

Instances

Instances details
Rename ImpName Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: ImpName PName -> RenameM (ImpName Name) Source #

Generic (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImpName name) 
Instance details

Defined in Cryptol.Parser.AST

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

Methods

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

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

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

Defined in Cryptol.Parser.AST

Methods

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

show :: ImpName name -> String #

showList :: [ImpName name] -> ShowS #

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

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: ImpName name -> ImpName name Source #

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

Defined in Cryptol.Parser.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ImpName name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ImpName name -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

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

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

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

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

type Rep (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

data ImportSpec Source #

The list of names following an import.

Constructors

Hiding [Ident] 
Only [Ident] 

Instances

Instances details
Generic ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ImportSpec 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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])))

Methods

from :: ImportSpec -> Rep ImportSpec x #

to :: Rep ImportSpec x -> ImportSpec #

Show ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImportSpec -> ShowS #

show :: ImportSpec -> String #

showList :: [ImportSpec] -> ShowS #

PP ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ImportSpec -> Doc Source #

NFData ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportSpec -> () #

Eq ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Hiding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])) :+: C1 ('MetaCons "Only" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])))

data ExportType Source #

Export information for a declaration.

Constructors

Public 
Private 

Instances

Instances details
Generic ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ExportType 
Instance details

Defined in Cryptol.Parser.AST

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

Methods

from :: ExportType -> Rep ExportType x #

to :: Rep ExportType x -> ExportType #

Show ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ExportType -> ShowS #

show :: ExportType -> String #

showList :: [ExportType] -> ShowS #

NFData ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ExportType -> () #

Eq ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Ord ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

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 #

type Rep ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

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

newtype ExportSpec name Source #

Constructors

ExportSpec (Map Namespace (Set name)) 

Instances

Instances details
Ord name => Monoid (ExportSpec name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Exports

Methods

mempty :: ExportSpec name #

mappend :: ExportSpec name -> ExportSpec name -> ExportSpec name #

mconcat :: [ExportSpec name] -> ExportSpec name #

Ord name => Semigroup (ExportSpec name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Exports

Methods

(<>) :: ExportSpec name -> ExportSpec name -> ExportSpec name #

sconcat :: NonEmpty (ExportSpec name) -> ExportSpec name #

stimes :: Integral b => b -> ExportSpec name -> ExportSpec name #

Generic (ExportSpec name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Exports

Associated Types

type Rep (ExportSpec name) 
Instance details

Defined in Cryptol.ModuleSystem.Exports

type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'True) (C1 ('MetaCons "ExportSpec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Namespace (Set name)))))

Methods

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

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

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

Defined in Cryptol.ModuleSystem.Exports

Methods

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

show :: ExportSpec name -> String #

showList :: [ExportSpec name] -> ShowS #

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

Defined in Cryptol.IR.TraverseNames

Methods

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

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

Defined in Cryptol.ModuleSystem.Exports

Methods

rnf :: ExportSpec name -> () #

type Rep (ExportSpec name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Exports

type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'True) (C1 ('MetaCons "ExportSpec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Namespace (Set name)))))

isExportedBind :: Ord name => name -> ExportSpec name -> Bool Source #

Check to see if a binding is exported.

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

Check to see if a type synonym is exported.

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

data Pragma Source #

Constructors

PragmaNote String 
PragmaProperty 

Instances

Instances details
Generic Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep Pragma 
Instance details

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Pragma -> Rep Pragma x #

to :: Rep Pragma x -> Pragma #

Show Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Pragma -> ShowS #

show :: Pragma -> String #

showList :: [Pragma] -> ShowS #

NoPos Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma Source #

PP Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Pragma -> Doc Source #

NFData Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Pragma -> () #

Eq Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type))

data Fixity Source #

Constructors

Fixity 

Fields

Instances

Instances details
Generic Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Associated Types

type Rep Fixity 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

Methods

from :: Fixity -> Rep Fixity x #

to :: Rep Fixity x -> Fixity #

Show Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS #

show :: Fixity -> String #

showList :: [Fixity] -> ShowS #

PP Fixity Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

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

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> Fixity -> Doc Source #

NFData Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Fixity -> () #

Eq Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

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

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

Ord Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

compare :: Fixity -> Fixity -> Ordering #

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

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

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

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

max :: Fixity -> Fixity -> Fixity #

min :: Fixity -> Fixity -> Fixity #

type Rep Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

data PrimMap Source #

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

Constructors

PrimMap 

Fields

Instances

Instances details
Semigroup PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

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

sconcat :: NonEmpty PrimMap -> PrimMap #

stimes :: Integral b => b -> PrimMap -> PrimMap #

Generic PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Associated Types

type Rep PrimMap 
Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

Methods

from :: PrimMap -> Rep PrimMap x #

to :: Rep PrimMap x -> PrimMap #

Show PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> PrimMap -> ShowS #

show :: PrimMap -> String #

showList :: [PrimMap] -> ShowS #

NFData PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: PrimMap -> () #

type Rep PrimMap Source # 
Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

data FFI Source #

Constructors

CallC (FFIFunType FFIType) 
CallAbstract (FFIFunType Type) 

Instances

Instances details
Generic FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Associated Types

type Rep FFI 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep FFI = D1 ('MetaData "FFI" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "CallC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType FFIType))) :+: C1 ('MetaCons "CallAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType Type))))

Methods

from :: FFI -> Rep FFI x #

to :: Rep FFI x -> FFI #

Show FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

showsPrec :: Int -> FFI -> ShowS #

show :: FFI -> String #

showList :: [FFI] -> ShowS #

FreeVars FFI Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: FFI -> Deps Source #

TraverseNames FFI Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

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

ShowParseable FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: FFI -> Doc Void Source #

NFData FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

rnf :: FFI -> () #

type Rep FFI Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

type Rep FFI = D1 ('MetaData "FFI" "Cryptol.TypeCheck.AST" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "CallC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType FFIType))) :+: C1 ('MetaCons "CallAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FFIFunType Type))))