| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.TypeCheck.AST
Description
- data Module = Module {}
- data Expr
- data Match
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- groupDecls :: DeclGroup -> [Decl]
- data Decl = Decl {}
- data DeclDef
- ePrim :: PrimMap -> Ident -> Expr
- eError :: PrimMap -> Type -> String -> Expr
- eString :: PrimMap -> String -> Expr
- eChar :: PrimMap -> Char -> Expr
- ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
- splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
- splitAbs :: Expr -> Maybe ((Name, Type), Expr)
- splitTAbs :: Expr -> Maybe (TParam, Expr)
- splitProofAbs :: Expr -> Maybe (Prop, Expr)
- data Name
- data TFun
- data Selector
- data Import = Import {}
- data ImportSpec
- data ExportType
- data ExportSpec name = ExportSpec {}
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- data Pragma
- data Fixity = Fixity {}
- data PrimMap = PrimMap {}
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- module Cryptol.TypeCheck.Type
Documentation
A Cryptol module.
Constructors
| Module | |
Constructors
| EList [Expr] Type | List value (with type of elements) |
| ETuple [Expr] | Tuple value |
| ERec [(Ident, Expr)] | Record value |
| ESel Expr Selector | Elimination for tuplerecordlist |
| EIf Expr Expr Expr | If-then-else |
| EComp Type Type Expr [[Match]] | List comprehensions The types cache the length of the sequence and its element type. |
| EVar Name | Use of a bound variable |
| ETAbs TParam Expr | Function Value |
| ETApp Expr Type | Type application |
| EApp Expr Expr | Function application |
| EAbs Name Type Expr | Function value |
| EProofAbs Prop Expr | Proof abstraction. Because we don't keep proofs around
we don't need to name the assumption, but we still need to
record the assumption. The assumption is the |
| EProofApp Expr | If `e : p => t`, then `EProofApp e : t`,
as long as we can prove 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] |
Constructors
| Recursive [Decl] | Mutually recursive declarations |
| NonRecursive Decl | Non-recursive declaration |
groupDecls :: DeclGroup -> [Decl] Source #
Constructors
| Decl | |
ePrim :: PrimMap -> Ident -> Expr Source #
Construct a primitive, given a map to the unique names of the Cryptol module.
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 #
Built-in 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 |
| TCLenFromThen |
|
| TCLenFromThenTo |
|
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.
An import declaration.
data ImportSpec Source #
The list of names following an import.
INVARIANT: All of the Name entries in the list are expected to be
unqualified names; the QName or NewName constructors should not be
present.
Instances
data ExportSpec name Source #
Constructors
| ExportSpec | |
Instances
| Show name => Show (ExportSpec name) Source # | |
| Generic (ExportSpec name) Source # | |
| Ord name => Monoid (ExportSpec name) Source # | |
| NFData name => NFData (ExportSpec name) Source # | |
| type Rep (ExportSpec name) Source # | |
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.
Constructors
| PragmaNote String | |
| PragmaProperty |
A mapping from an identifier defined in some module to its real name.
data TCErrorMessage Source #
Constructors
| TCErrorMessage | |
Fields
| |
module Cryptol.TypeCheck.Type