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