| 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 Kind
- data Schema = Forall {}
- data TySyn = TySyn {}
- data Newtype = Newtype {}
- data TParam = TParam {}
- tpVar :: TParam -> TVar
- data Type
- type Prop = Type
- type SType = Type
- data TVar
- data TCon
- data PC
- data TC
- data UserTC = UserTC Name Kind
- data Expr
- data Match
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- groupDecls :: DeclGroup -> [Decl]
- data Decl = Decl {}
- data DeclDef
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsNat' :: Type -> Maybe Nat'
- tIsNum :: Type -> Maybe Integer
- tIsInf :: Type -> Bool
- tIsVar :: Type -> Maybe TVar
- tIsFun :: Type -> Maybe (Type, Type)
- tIsSeq :: Type -> Maybe (Type, Type)
- tIsBit :: Type -> Bool
- tIsTuple :: Type -> Maybe [Type]
- tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
- tSplitFun :: TFun -> Type -> [Type]
- pIsFin :: Prop -> Maybe Type
- pIsGeq :: Prop -> Maybe (Type, Type)
- pIsEq :: Prop -> Maybe (Type, Type)
- pIsArith :: Prop -> Maybe Type
- pIsCmp :: Prop -> Maybe Type
- pIsNumeric :: Prop -> Bool
- tNum :: Integral a => a -> Type
- tZero :: Type
- tOne :: Type
- tTwo :: Type
- tInf :: Type
- tNat' :: Nat' -> Type
- tBit :: Type
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: [(Ident, Type)] -> Type
- tTuple :: [Type] -> Type
- tFun :: Type -> Type -> Type
- tNoUser :: Type -> Type
- tWidth :: Type -> Type
- tLenFromThen :: Type -> Type -> Type -> Type
- tLenFromThenTo :: Type -> Type -> Type -> Type
- tMax :: Type -> Type -> Type
- (=#=) :: Type -> Type -> Prop
- (=/=) :: Type -> Type -> Prop
- pArith :: Type -> Prop
- pCmp :: Type -> Prop
- (>==) :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pFin :: Type -> Prop
- (.*.) :: Type -> Type -> Type
- (.+.) :: Type -> Type -> Type
- (.-.) :: Type -> Type -> Type
- (.^.) :: Type -> Type -> Type
- tDiv :: Type -> Type -> Type
- tMod :: Type -> Type -> Type
- tMin :: Type -> Type -> Type
- newtypeTyCon :: Newtype -> TCon
- newtypeConType :: Newtype -> Schema
- ePrim :: PrimMap -> Ident -> Expr
- eError :: PrimMap -> Type -> String -> Expr
- eString :: PrimMap -> String -> Expr
- eChar :: PrimMap -> Char -> Expr
- class HasKind t where
- quickApply :: Kind -> [a] -> Kind
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- 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 {}
Documentation
A Cryptol module.
Constructors
| Module | |
Kinds, classify types.
The types of polymorphic values.
Instances
| Eq Schema Source | |
| Show Schema Source | |
| Generic Schema Source | |
| NFData Schema Source | |
| PP Schema Source | |
| TVars Schema Source | WARNING: This instance assumes that the quantified variables in the types in the substitution will not get captured by the quantified variables. This is reasonable because there should be no shadowing of quantified variables but, just in case, we make a sanity check and panic if somehow capture did occur. |
| FVS Schema Source | |
| PP (WithNames Schema) Source | |
| type Rep Schema Source |
Type synonym.
Constructors
| TySyn | |
Named records
Constructors
| Newtype | |
Type parameters.
Constructors
| TParam | |
The internal representation of types. These are assumed to be kind correct.
Constructors
| TCon TCon [Type] | Type constant with args |
| TVar TVar | Type variable (free or bound) |
| TUser Name [Type] Type | This is just a type annotation, for a type that
was written as a type synonym. It is useful so that we
can use it to report nicer errors.
Example: `TUser T ts t` is really just the type |
| TRec [(Ident, Type)] | Record type |
Type variables.
Type constants.
Built-in type constants.
Predicate symbols.
1-1 constants.
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 Expr [[Match]] | List comprehensions The type caches the type of the expr. |
| 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. |
| ECast Expr Type | if e : t1, then cast e : t2 as long as we can prove that 't1 = t2'. We could express this in terms of a built-in constant. `cast :: {a,b} (a =*= b) => a -> b` Using the constant is a bit verbose though, because we end up with both the source and target type. So, instead we use this language construct, which only stores the target type, and the source type can be reconstructed from the expression. Another way to think of this is simply as an expression with an explicit type annotation. |
| EWhere Expr [DeclGroup] |
Constructors
| Recursive [Decl] | Mutually recursive declarations |
| NonRecursive Decl | Non-recursive declaration |
groupDecls :: DeclGroup -> [Decl] Source
Constructors
| Decl | |
tSplitFun :: TFun -> Type -> [Type] Source
Split up repeated occurances of the given binary type-level function.
pIsNumeric :: Prop -> Bool Source
pHas :: Selector -> Type -> Type -> Prop Source
A Has constraint, used for tuple and record selection.
newtypeTyCon :: Newtype -> TCon Source
newtypeConType :: Newtype -> Schema Source
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.
quickApply :: Kind -> [a] -> Kind Source
ppNewtypeShort :: Newtype -> Doc Source
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 |