cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell2010

Cryptol.TypeCheck.AST

Description

Synopsis

- type Module = ModuleG ModName
- data Expr
  - = EList [Expr] Type
  - | ETuple [Expr]
  - | ERec (RecordMap Ident Expr)
  - | ESel Expr Selector
  - | ESet Type Expr Selector Expr
  - | EIf Expr Expr Expr
  - | EComp Type Type Expr [[Match]]
  - | EVar Name
  - | ETAbs TParam Expr
  - | ETApp Expr Type
  - | EApp Expr Expr
  - | EAbs Name Type Expr
  - | ELocated Range Expr
  - | EProofAbs Prop Expr
  - | EProofApp Expr
  - | EWhere Expr [DeclGroup]
  - | EPropGuards [([Prop], Expr)] Type
- data Match
  - = From Name Type Type Expr
  - | Let Decl
- data ModuleG mname = Module {
  - mName :: !mname
  - mDoc :: !(Maybe Text)
  - mExports :: ExportSpec Name
  - mParamTypes :: Map Name ModTParam
  - mParamFuns :: Map Name ModVParam
  - mParamConstraints :: [Located Prop]
  - mParams :: FunctorParams
  - mFunctors :: Map Name (ModuleG Name)
  - mNested :: !(Set Name)
  - mTySyns :: Map Name TySyn
  - mNewtypes :: Map Name Newtype
  - mPrimTypes :: Map Name AbstractType
  - mDecls :: [DeclGroup]
  - mSubmodules :: Map Name (IfaceNames Name)
  - mSignatures :: !(Map Name ModParamNames)
  }
- data Decl = Decl {
  - dName :: !Name
  - dSignature :: Schema
  - dDefinition :: DeclDef
  - dPragmas :: [Pragma]
  - dInfix :: !Bool
  - dFixity :: Maybe Fixity
  - dDoc :: Maybe Text
  }
- data TCTopEntity
  - = TCTopModule (ModuleG ModName)
  - | TCTopSignature ModName ModParamNames
- data DeclGroup
  - = Recursive [Decl]
  - | NonRecursive Decl
- data DeclDef
  - = DPrim
  - | DForeign FFIFunType
  - | DExpr Expr
- splitTApp :: Expr -> Maybe (Type, Expr)
- findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)]
- splitApp :: Expr -> Maybe (Expr, Expr)
- tcTopEntitytName :: TCTopEntity -> ModName
- tcTopEntityToModule :: TCTopEntity -> Module
- emptyModule :: mname -> ModuleG mname
- findForeignDeclsInFunctors :: ModuleG mname -> [Name]
- isParametrizedModule :: ModuleG mname -> Bool
- groupDecls :: DeclGroup -> [Decl]
- ePrim :: PrimMap -> PrimIdent -> Expr
- eError :: PrimMap -> Type -> String -> Expr
- eString :: PrimMap -> String -> Expr
- eChar :: PrimMap -> Char -> Expr
- splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
- splitAbs :: Expr -> Maybe ((Name, Type), Expr)
- ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
- splitProofAbs :: Expr -> Maybe (Prop, Expr)
- splitTAbs :: Expr -> Maybe (TParam, Expr)
- splitLoc :: Expr -> Maybe (Range, Expr)
- dropLocs :: Expr -> Expr
- splitProofApp :: Expr -> Maybe ((), Expr)
- splitExprInst :: Expr -> (Expr, [Type], Int)
- data Name
- data TFun
  - = TCAdd
  - | TCSub
  - | TCMul
  - | TCDiv
  - | TCMod
  - | TCExp
  - | TCWidth
  - | TCMin
  - | TCMax
  - | TCCeilDiv
  - | TCCeilMod
  - | TCLenFromThenTo
- data Selector
  - = TupleSel Int (Maybe Int)
  - | RecordSel Ident (Maybe [Ident])
  - | ListSel Int (Maybe Int)
- type Import = ImportG ModName
- data ImportG mname = Import {
  - iModule :: !mname
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  - iInst :: !(Maybe (ModuleInstanceArgs PName))
  }
- data ImpName name
  - = ImpTop ModName
  - | ImpNested name
- data ImportSpec
  - = Hiding [Ident]
  - | Only [Ident]
- data ExportType
  - = Public
  - | Private
- newtype ExportSpec name = ExportSpec (Map Namespace (Set name))
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool
- data Pragma
  - = PragmaNote String
  - | PragmaProperty
- data Fixity = Fixity {
  - fAssoc :: !Assoc
  - fLevel :: !Int
  }
- data PrimMap = PrimMap {
  - primDecls :: Map PrimIdent Name
  - primTypes :: Map PrimIdent Name
  }
- module Cryptol.TypeCheck.Type

# Documentation

type Module = ModuleG ModName Source #

data Expr Source #

Constructors

EList [Expr] Type | List value (with type of elements)
ETuple [Expr] | Tuple value
ERec (RecordMap Ident Expr) | Record value
ESel Expr Selector | Elimination for tuplerecordlist
ESet Type Expr Selector Expr | Change the value of a field. The included type gives the type of the record being updated
EIf Expr Expr Expr | If-then-else
EComp Type Type Expr [[Match]] | List comprehensions The types cache the length of the sequence and its element type.
EVar Name | Use of a bound variable
ETAbs TParam Expr | Function Value
ETApp Expr Type | Type application
EApp Expr Expr | Function application
EAbs Name Type Expr | Function value
ELocated Range Expr | Source location information
EProofAbs Prop Expr | Proof abstraction. Because we don't keep proofs around we don't need to name the assumption, but we still need to record the assumption. The assumption is the `Type` term, which should be of kind `KProp`.
EProofApp Expr | If `e : p => t`, then `EProofApp e : t`, as long as we can prove `p`. We don't record the actual proofs, as they are not used for anything. It may be nice to keep them around for sanity checking.
EWhere Expr [DeclGroup] |
EPropGuards [([Prop], Expr)] Type |

#### Instances

Instances details

Generic Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Expr :: Type -> Type Source # Methods from :: Expr -> Rep Expr x Source # to :: Rep Expr x -> Expr Source #
Show Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
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 #
NFData Expr Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Expr -> () Source #
PP (WithNames Expr) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Expr -> Doc Source #
type Rep Expr Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Expr = D1 ('MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 "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 Match Source #

Constructors

From Name Type Type Expr | Type arguments are the length and element type of the sequence expression
Let Decl |

#### Instances

Instances details

Generic Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Match :: Type -> Type Source # Methods from :: Match -> Rep Match x Source # to :: Rep Match x -> Match Source #
Show Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Match -> ShowS Source # show :: Match -> String Source # showList :: [Match] -> ShowS Source #
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 #
NFData Match Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Match -> () Source #
PP (WithNames Match) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Match -> Doc Source #
type Rep Match Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Match = D1 ('MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 ModuleG mname Source #

A Cryptol module.

Constructors

Module |

Fields

- mName :: !mname
- mDoc :: !(Maybe Text)
- mExports :: ExportSpec Name
- mParamTypes :: Map Name ModTParam
- mParamFuns :: Map Name ModVParam
- mParamConstraints :: [Located Prop]
- mParams :: FunctorParams

  Parameters grouped by "import".

- mFunctors :: Map Name (ModuleG Name)

  Functors directly nested in this module. Things further nested are in the modules in the elements of the map.

- mNested :: !(Set Name)

  Submodules, functors, and interfaces nested directly in this module

- mTySyns :: Map Name TySyn
- mNewtypes :: Map Name Newtype
- mPrimTypes :: Map Name AbstractType
- mDecls :: [DeclGroup]
- mSubmodules :: Map Name (IfaceNames Name)
- mSignatures :: !(Map Name ModParamNames)

#### Instances

Instances details

Generic (ModuleG mname) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep (ModuleG mname) :: Type -> Type Source # Methods from :: ModuleG mname -> Rep (ModuleG mname) x Source # to :: Rep (ModuleG mname) x -> ModuleG mname Source #
Show mname => Show (ModuleG mname) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> ModuleG mname -> ShowS Source # show :: ModuleG mname -> String Source # showList :: [ModuleG mname] -> ShowS Source #
ModuleInstance (ModuleG name) Source # |
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModuleG name -> ModuleG name Source #
TVars (ModuleG names) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> ModuleG names -> ModuleG names Source #
PP n => PP (ModuleG n) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> ModuleG n -> Doc Source #
PP n => PP (WithNames (ModuleG n)) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames (ModuleG n) -> Doc Source #
NFData mname => NFData (ModuleG mname) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: ModuleG mname -> () Source #
type Rep (ModuleG mname) Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep (ModuleG mname) = D1 ('MetaData "ModuleG" "Cryptol.TypeCheck.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 mname) :*: (S1 ('MetaSel ('Just "mDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe 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 "mNewtypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name Newtype)))) :*: ((S1 ('MetaSel ('Just "mPrimTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name AbstractType)) :*: S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup])) :*: (S1 ('MetaSel ('Just "mSubmodules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name (IfaceNames Name))) :*: S1 ('MetaSel ('Just "mSignatures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name ModParamNames)))))))

data Decl Source #

Constructors

Decl |

Fields

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

#### Instances

Instances details

Generic Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep Decl :: Type -> Type Source # Methods from :: Decl -> Rep Decl x Source # to :: Rep Decl x -> Decl Source #
Show Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> Decl -> ShowS Source # show :: Decl -> String Source # showList :: [Decl] -> ShowS Source #
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 #
NFData Decl Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: Decl -> () Source #
PP (WithNames Decl) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Decl -> Doc Source #
type Rep Decl Source # |

Instance details

Defined in Cryptol.TypeCheck.AST

type Rep Decl = D1 ('MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 :: Type -> Type Source # Methods from :: TCTopEntity -> Rep TCTopEntity x Source # to :: Rep TCTopEntity x -> TCTopEntity Source #
Show TCTopEntity Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> TCTopEntity -> ShowS Source # show :: TCTopEntity -> String Source # showList :: [TCTopEntity] -> ShowS Source #
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 #
NFData TCTopEntity Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: TCTopEntity -> () Source #
PP (WithNames TCTopEntity) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: 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.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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)))

data DeclGroup Source #

Constructors

Recursive [Decl] | Mutually recursive declarations
NonRecursive Decl | Non-recursive declaration

#### Instances

Instances details

Generic DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclGroup :: Type -> Type Source # Methods from :: DeclGroup -> Rep DeclGroup x Source # to :: Rep DeclGroup x -> DeclGroup Source #
Show DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> DeclGroup -> ShowS Source # show :: DeclGroup -> String Source # showList :: [DeclGroup] -> ShowS Source #
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 #
NFData DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods rnf :: DeclGroup -> () Source #
PP (WithNames DeclGroup) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: 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.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 DeclDef Source #

Constructors

DPrim |
DForeign FFIFunType |
DExpr Expr |

#### Instances

Instances details

Generic DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.AST Associated Types type Rep DeclDef :: Type -> Type Source # Methods from :: DeclDef -> Rep DeclDef x Source # to :: Rep DeclDef x -> DeclDef Source #
Show DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods showsPrec :: Int -> DeclDef -> ShowS Source # show :: DeclDef -> String Source # showList :: [DeclDef] -> ShowS Source #
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 -> () Source #
PP (WithNames DeclDef) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: 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.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DForeign" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIFunType)) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

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

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

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

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

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. This is used to report an error

isParametrizedModule :: ModuleG mname -> Bool Source #

Is this a parameterized module?

groupDecls :: DeclGroup -> [Decl] Source #

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 #

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 :: Type -> Type Source # Methods from :: Name -> Rep Name x Source # to :: Rep Name x -> Name Source #
Show Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
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 #
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 -> () Source #
Eq Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
type Rep Name Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source # maxBound :: TFun Source #
Enum TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods succ :: TFun -> TFun Source # pred :: TFun -> TFun Source # toEnum :: Int -> TFun Source # fromEnum :: TFun -> Int Source # enumFrom :: TFun -> [TFun] Source # enumFromThen :: TFun -> TFun -> [TFun] Source # enumFromTo :: TFun -> TFun -> [TFun] Source # enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] Source #
Generic TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Associated Types type Rep TFun :: Type -> Type Source # Methods from :: TFun -> Rep TFun x Source # to :: Rep TFun x -> TFun Source #
Show TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods showsPrec :: Int -> TFun -> ShowS Source # show :: TFun -> String Source # showList :: [TFun] -> ShowS Source #
HasKind TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods kindOf :: TFun -> Kind Source #
PP TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods ppPrec :: Int -> TFun -> Doc Source #
NFData TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods rnf :: TFun -> () Source #
Eq TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods (==) :: TFun -> TFun -> Bool Source # (/=) :: TFun -> TFun -> Bool Source #
Ord TFun Source # |
Instance details Defined in Cryptol.TypeCheck.TCon Methods compare :: TFun -> TFun -> Ordering Source # (<) :: TFun -> TFun -> Bool Source # (<=) :: TFun -> TFun -> Bool Source # (>) :: TFun -> TFun -> Bool Source # (>=) :: TFun -> TFun -> Bool Source # max :: TFun -> TFun -> TFun Source # min :: TFun -> TFun -> TFun Source #
type Rep TFun Source # |

Instance details

Defined in Cryptol.TypeCheck.TCon

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

data Selector Source #

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

Constructors

TupleSel Int (Maybe Int) | Zero-based tuple selection. Optionally specifies the shape of the tuple (one-based).
RecordSel Ident (Maybe [Ident]) | Record selection. Optionally specifies the shape of the record.
ListSel Int (Maybe Int) | List selection. Optionally specifies the length of the list.

#### Instances

Instances details

Generic Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Associated Types type Rep Selector :: Type -> Type Source # Methods from :: Selector -> Rep Selector x Source # to :: Rep Selector x -> Selector Source #
Show Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods showsPrec :: Int -> Selector -> ShowS Source # show :: Selector -> String Source # showList :: [Selector] -> ShowS Source #
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 #
NFData Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods rnf :: Selector -> () Source #
Eq Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods (==) :: Selector -> Selector -> Bool Source # (/=) :: Selector -> Selector -> Bool Source #
Ord Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods compare :: Selector -> Selector -> Ordering Source # (<) :: Selector -> Selector -> Bool Source # (<=) :: Selector -> Selector -> Bool Source # (>) :: Selector -> Selector -> Bool Source # (>=) :: Selector -> Selector -> Bool Source # max :: Selector -> Selector -> Selector Source # min :: Selector -> Selector -> Selector Source #
type Rep Selector Source # |

Instance details

Defined in Cryptol.Parser.Selector

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

- iModule :: !mname
- iAs :: Maybe ModName
- iSpec :: Maybe ImportSpec
- iInst :: !(Maybe (ModuleInstanceArgs PName))

  `iInst` exists only during parsing

#### Instances

Instances details

Generic (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ImportG mname) :: Type -> Type Source # Methods from :: ImportG mname -> Rep (ImportG mname) x Source # to :: Rep (ImportG mname) x -> ImportG mname Source #
Show mname => Show (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportG mname -> ShowS Source # show :: ImportG mname -> String Source # showList :: [ImportG mname] -> ShowS Source #
PP mname => PP (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportG mname -> Doc Source #
NFData mname => NFData (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportG mname -> () Source #
type Rep (ImportG mname) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) ((S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 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))))))

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) :: Type -> Type Source # Methods from :: ImpName name -> Rep (ImpName name) x Source # to :: Rep (ImpName name) x -> ImpName name Source #
Show name => Show (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImpName name -> ShowS Source # show :: ImpName name -> String Source # showList :: [ImpName name] -> ShowS Source #
ModuleInstance name => ModuleInstance (ImpName name) Source # |
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ImpName name -> ImpName name Source #
PP name => PP (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImpName name -> Doc Source #
NFData name => NFData (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImpName name -> () Source #
Eq name => Eq (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImpName name -> ImpName name -> Bool Source # (/=) :: ImpName name -> ImpName name -> Bool Source #
Ord name => Ord (ImpName name) Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

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

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

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

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

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

type Rep (ImpName name) Source # |

Instance details

Defined in Cryptol.Parser.AST

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

data ImportSpec Source #

The list of names following an import.

Constructors

Hiding [Ident] |
Only [Ident] |

#### Instances

Instances details

Generic ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type Source # Methods from :: ImportSpec -> Rep ImportSpec x Source # to :: Rep ImportSpec x -> ImportSpec Source #
Show ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS Source # show :: ImportSpec -> String Source # showList :: [ImportSpec] -> ShowS Source #
PP ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source #
NFData ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () Source #
Eq ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImportSpec -> ImportSpec -> Bool Source # (/=) :: ImportSpec -> ImportSpec -> Bool Source #
type Rep ImportSpec Source # |

Instance details

Defined in Cryptol.Parser.AST

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

data ExportType Source #

Export information for a declaration.

Constructors

Public |
Private |

#### Instances

Instances details

Generic ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type Source # Methods from :: ExportType -> Rep ExportType x Source # to :: Rep ExportType x -> ExportType Source #
Show ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS Source # show :: ExportType -> String Source # showList :: [ExportType] -> ShowS Source #
NFData ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () Source #
Eq ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ExportType -> ExportType -> Bool Source # (/=) :: ExportType -> ExportType -> Bool Source #
Ord ExportType Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ExportType -> ExportType -> Ordering Source #

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

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

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

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

max :: ExportType -> ExportType -> ExportType Source #

min :: ExportType -> ExportType -> ExportType Source #

type Rep ExportType Source # |
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source # mappend :: ExportSpec name -> ExportSpec name -> ExportSpec name Source # mconcat :: [ExportSpec name] -> ExportSpec name Source #
Ord name => Semigroup (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Methods (<>) :: ExportSpec name -> ExportSpec name -> ExportSpec name Source # sconcat :: NonEmpty (ExportSpec name) -> ExportSpec name Source # stimes :: Integral b => b -> ExportSpec name -> ExportSpec name Source #
Generic (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Associated Types type Rep (ExportSpec name) :: Type -> Type Source # Methods from :: ExportSpec name -> Rep (ExportSpec name) x Source # to :: Rep (ExportSpec name) x -> ExportSpec name Source #
Show name => Show (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports Methods showsPrec :: Int -> ExportSpec name -> ShowS Source # show :: ExportSpec name -> String Source # showList :: [ExportSpec name] -> ShowS Source #
(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 -> () Source #
type Rep (ExportSpec name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Exports type Rep (ExportSpec name) = D1 ('MetaData "ExportSpec" "Cryptol.ModuleSystem.Exports" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 :: Type -> Type Source # Methods from :: Pragma -> Rep Pragma x Source # to :: Rep Pragma x -> Pragma Source #
Show Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
NoPos Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pragma -> Pragma Source #
PP Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pragma -> Doc Source #
NFData Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pragma -> () Source #
Eq Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool Source #
type Rep Pragma Source # |
Instance details Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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

- fAssoc :: !Assoc
- fLevel :: !Int

#### Instances

Instances details

Generic Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Associated Types type Rep Fixity :: Type -> Type Source # Methods from :: Fixity -> Rep Fixity x Source # to :: Rep Fixity x -> Fixity Source #
Show Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods showsPrec :: Int -> Fixity -> ShowS Source # show :: Fixity -> String Source # showList :: [Fixity] -> ShowS Source #
PP Fixity Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Fixity -> Doc Source #
NFData Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods rnf :: Fixity -> () Source #
Eq Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods (==) :: Fixity -> Fixity -> Bool Source # (/=) :: Fixity -> Fixity -> Bool Source #
Ord Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods compare :: Fixity -> Fixity -> Ordering Source # (<) :: Fixity -> Fixity -> Bool Source # (<=) :: Fixity -> Fixity -> Bool Source # (>) :: Fixity -> Fixity -> Bool Source # (>=) :: Fixity -> Fixity -> Bool Source # max :: Fixity -> Fixity -> Fixity Source # min :: Fixity -> Fixity -> Fixity Source #
type Rep Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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

- primDecls :: Map PrimIdent Name
- primTypes :: Map PrimIdent Name

#### Instances

Instances details

Semigroup PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (<>) :: PrimMap -> PrimMap -> PrimMap Source # sconcat :: NonEmpty PrimMap -> PrimMap Source # stimes :: Integral b => b -> PrimMap -> PrimMap Source #
Generic PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep PrimMap :: Type -> Type Source # Methods from :: PrimMap -> Rep PrimMap x Source # to :: Rep PrimMap x -> PrimMap Source #
Show PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS Source # show :: PrimMap -> String Source # showList :: [PrimMap] -> ShowS Source #
NFData PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: PrimMap -> () Source #
type Rep PrimMap Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

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