Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- 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 QName Kind
- data Expr
- data Match
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- groupDecls :: DeclGroup -> [Decl]
- data Decl = Decl {
- dName :: QName
- dSignature :: Schema
- dDefinition :: Expr
- dPragmas :: [Pragma]
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- 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]
- 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
- tBit :: Type
- eTrue :: Expr
- eFalse :: Expr
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- eChar :: Char -> Expr
- tString :: Int -> Type
- eString :: String -> Expr
- eError :: Type -> String -> Expr
- tRec :: [(Name, 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
- class HasKind t where
- quickApply :: Kind -> [a] -> Kind
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(QName, Type)] -> Expr -> Doc
- splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
- splitAbs :: Expr -> Maybe ((QName, Type), Expr)
- splitTAbs :: Expr -> Maybe (TParam, Expr)
- splitProofAbs :: Expr -> Maybe (Prop, Expr)
- data TFun
- data Name
- data QName = QName (Maybe ModName) Name
- mkUnqual :: Name -> QName
- unqual :: QName -> Name
- newtype ModName = ModName [String]
- data Selector
- data Import = Import {}
- data ImportSpec
- data ExportType
- data ExportSpec = ExportSpec {}
- isExportedBind :: QName -> ExportSpec -> Bool
- isExportedType :: QName -> ExportSpec -> Bool
- data Pragma
Documentation
A Cryptol module.
Kinds, classify types.
The types of polymorphic values.
Eq Schema Source | |
Show 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 synonym.
Named records
Type parameters.
The internal representation of types. These are assumed to be kind correct.
TCon TCon [Type] | Type constant with args |
TVar TVar | Type variable (free or bound) |
TUser QName [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 [(Name, Type)] | Record type |
Type variables.
Type constants.
Built-in type constants.
Predicate symbols.
1-1 constants.
ECon ECon | Built-in constant |
EList [Expr] Type | List value (with type of elements) |
ETuple [Expr] | Tuple value |
ERec [(Name, 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 QName | Use of a bound variable |
ETAbs TParam Expr | Function Value |
ETApp Expr Type | Type application |
EApp Expr Expr | Function application |
EAbs QName 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] |
Recursive [Decl] | Mutually recursive declarations |
NonRecursive Decl | Non-recursive declaration |
groupDecls :: DeclGroup -> [Decl] Source
Decl | |
|
pIsNumeric :: Prop -> Bool Source
eError :: Type -> String -> Expr Source
Make an expression that is error
pre-applied to a type and a
message.
pHas :: Selector -> Type -> Type -> Prop Source
A Has
constraint, used for tuple and record selection.
newtypeTyCon :: Newtype -> TCon Source
newtypeConType :: Newtype -> Schema Source
quickApply :: Kind -> [a] -> Kind Source
ppNewtypeShort :: Newtype -> Doc Source
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source
Built-in types.
TCAdd | : Num -> Num -> Num |
TCSub | : Num -> Num -> Num |
TCMul | : Num -> Num -> Num |
TCDiv | : Num -> Num -> Num |
TCMod | : Num -> Num -> Num |
TCLg2 | : Num -> Num |
TCExp | : Num -> Num -> Num |
TCWidth | : Num -> Num |
TCMin | : Num -> Num -> Num |
TCMax | : Num -> Num -> Num |
TCLenFromThen |
|
TCLenFromThenTo |
|
Module names are just namespaces.
INVARIANT: the list of strings should never be empty in a valid module name.
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
data ExportType Source
Export information for a declaration.
data ExportSpec Source
isExportedBind :: QName -> ExportSpec -> Bool Source
Check to see if a binding is exported.
isExportedType :: QName -> ExportSpec -> Bool Source
Check to see if a type synonym is exported.