| 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 Match
- data Expr
- = EList [Expr] Type
- | ETuple [Expr]
- | ERec (RecordMap Ident Expr)
- | ESel Expr Selector
- | ESet Type Expr Selector Expr
- | EIf Expr Expr Expr
- | ECase Expr (Map Ident CaseAlt) (Maybe CaseAlt)
- | 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 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
- mNominalTypes :: Map Name NominalType
- mDecls :: [DeclGroup]
- mSubmodules :: Map Name (IfaceNames Name)
- mSignatures :: !(Map Name ModParamNames)
- mInScope :: NamingEnv
- data Decl = Decl {}
- data CaseAlt = CaseAlt [(Name, Type)] Expr
- data TCTopEntity
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- data DeclDef
- 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
- groupDecls :: DeclGroup -> [Decl]
- findForeignDeclsInFunctors :: ModuleG mname -> [Name]
- isParametrizedModule :: ModuleG mname -> Bool
- 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
- data Selector
- type Import = ImportG ModName
- data ImportG mname = Import {}
- data ImpName name
- data ImportSpec
- data ExportType
- 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
- data Fixity = Fixity {}
- data PrimMap = PrimMap {}
- module Cryptol.TypeCheck.Type
Documentation
Constructors
| From Name Type Type Expr | Type arguments are the length and element type of the sequence expression |
| Let Decl |
Instances
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
|
| 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 |
| EProofApp Expr | If 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
A Cryptol module.
Constructors
| Module | |
Fields
| |
Instances
Constructors
| Decl | |
Instances
Used for case expressions. Similar to a lambda, the variables are bound by the value examined in the case.
Instances
| Generic CaseAlt Source # | |
| Show CaseAlt Source # | |
| FreeVars CaseAlt Source # | |
| TraverseNames CaseAlt Source # | |
Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => CaseAlt -> f CaseAlt Source # | |
| ShowParseable CaseAlt Source # | |
Defined in Cryptol.TypeCheck.Parseable | |
| TVars CaseAlt Source # | |
| PP CaseAlt Source # | |
| NFData CaseAlt Source # | |
Defined in Cryptol.TypeCheck.AST | |
| type Rep CaseAlt Source # | |
Defined in Cryptol.TypeCheck.AST type Rep CaseAlt = D1 ('MetaData "CaseAlt" "Cryptol.TypeCheck.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 TCTopEntity Source #
Constructors
| TCTopModule (ModuleG ModName) | |
| TCTopSignature ModName ModParamNames |
Instances
Constructors
| Recursive [Decl] | Mutually recursive declarations |
| NonRecursive Decl | Non-recursive declaration |
Instances
Constructors
| DPrim | |
| DForeign FFIFunType (Maybe Expr) | Foreign functions can have an optional cryptol implementation |
| DExpr Expr |
Instances
findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)] Source #
Find all the foreign declarations in the module and return their names and FFIFunTypes.
tcTopEntityToModule :: TCTopEntity -> Module Source #
Panics if the entity is not a module
emptyModule :: mname -> ModuleG mname Source #
groupDecls :: DeclGroup -> [Decl] 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.
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source #
splitExprInst :: Expr -> (Expr, [Type], Int) Source #
Deconstruct an expression, typically polymorphic, into the types and proofs to which it is applied. Since we don't store the proofs, we just return the number of proof applications. The first type is the one closest to the expr.
Instances
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 |
|
Instances
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
An import declaration.
Constructors
| Import | |
Instances
| Generic (ImportG mname) Source # | |
| Show mname => Show (ImportG mname) Source # | |
| PP mname => PP (ImportG mname) Source # | |
| NFData mname => NFData (ImportG mname) Source # | |
Defined in Cryptol.Parser.AST | |
| type Rep (ImportG mname) Source # | |
Defined in Cryptol.Parser.AST type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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)))))) | |
The name of an imported module
Instances
| Rename ImpName Source # | |
| Generic (ImpName name) Source # | |
| Show name => Show (ImpName name) Source # | |
| ModuleInstance name => ModuleInstance (ImpName name) Source # | |
Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ImpName name -> ImpName name Source # | |
| PP name => PP (ImpName name) Source # | |
| NFData name => NFData (ImpName name) Source # | |
Defined in Cryptol.Parser.AST | |
| Eq name => Eq (ImpName name) Source # | |
| Ord name => Ord (ImpName name) Source # | |
Defined in Cryptol.Parser.AST | |
| type Rep (ImpName name) Source # | |
Defined in Cryptol.Parser.AST type Rep (ImpName name) = D1 ('MetaData "ImpName" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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.
Instances
| Generic ImportSpec Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type # | |
| Show ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS # show :: ImportSpec -> String # showList :: [ImportSpec] -> ShowS # | |
| PP ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
| NFData ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () # | |
| Eq ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
| type Rep ImportSpec Source # | |
Defined in Cryptol.Parser.AST type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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.
Instances
| Generic ExportType Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type # | |
| Show ExportType Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS # | |
| NFData ExportType Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () # | |
| Eq ExportType Source # | |
Defined in Cryptol.Parser.AST | |
| Ord ExportType Source # | |
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 # | |
newtype ExportSpec name Source #
Constructors
| ExportSpec (Map Namespace (Set name)) |
Instances
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 #
Constructors
| PragmaNote String | |
| PragmaProperty |
Instances
| Generic Pragma Source # | |
| Show Pragma Source # | |
| NoPos Pragma Source # | |
| PP Pragma Source # | |
| NFData Pragma Source # | |
Defined in Cryptol.Parser.AST | |
| Eq Pragma Source # | |
| type Rep Pragma Source # | |
Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type)) | |
Instances
| Generic Fixity Source # | |
| Show Fixity Source # | |
| PP Fixity Source # | |
| NFData Fixity Source # | |
Defined in Cryptol.Utils.Fixity | |
| Eq Fixity Source # | |
| Ord Fixity Source # | |
| type Rep Fixity Source # | |
Defined in Cryptol.Utils.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) | |
A mapping from an identifier defined in some module to its real name.
Instances
| Semigroup PrimMap Source # | |
| Generic PrimMap Source # | |
| Show PrimMap Source # | |
| NFData PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name | |
| type Rep PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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