cryptol-2.2.5: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.AST

Description

 

Synopsis

Documentation

data Kind Source

Kinds, classify types.

Constructors

KType 
KNum 
KProp 
Kind :-> Kind infixr 5 

data Schema Source

The types of polymorphic values.

Constructors

Forall 

Fields

sVars :: [TParam]
 
sProps :: [Prop]
 
sType :: Type
 

Instances

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 

data TySyn Source

Type synonym.

Constructors

TySyn 

Fields

tsName :: QName

Name

tsParams :: [TParam]

Parameters

tsConstraints :: [Prop]

Ensure body is OK

tsDef :: Type

Definition

data Newtype Source

Named records

Constructors

Newtype 

Fields

ntName :: QName
 
ntParams :: [TParam]
 
ntConstraints :: [Prop]
 
ntFields :: [(Name, Type)]
 

data TParam Source

Type parameters.

Constructors

TParam 

Fields

tpUnique :: !Int

Parameter identifier

tpKind :: Kind

Kind of parameter

tpName :: Maybe QName

Name from source, if any.

data Type Source

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 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 t that was written as `T ts` by the user.

TRec [(Name, Type)]

Record type

type Prop = Type Source

The type is supposed to be of kind KProp

type SType = Type Source

The type is "simple" (i.e., it contains no type functions).

data TVar Source

Type variables.

Constructors

TVFree !Int Kind (Set TVar) Doc

Unique, kind, ids of bound type variables that are in scope The Doc is a description of how this type came to be.

TVBound !Int Kind 

data TCon Source

Type constants.

Constructors

TC TC 
PC PC 
TF TFun 

data PC Source

Built-in type constants.

Predicate symbols.

Constructors

PEqual
_ == _
PNeq
_ /= _
PGeq
_ >= _
PFin
fin _
PHas Selector

Has sel type field does not appear in schemas

PArith
Arith _
PCmp
Cmp _

data TC Source

1-1 constants.

Constructors

TCNum Integer

Numbers

TCInf

Inf

TCBit

Bit

TCSeq
[_] _
TCFun
_ -> _
TCTuple Int
(_, _, _)
TCNewtype UserTC

user-defined, T

data Expr Source

Constructors

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 Type term, which should be of kind KProp.

EProofApp Expr

If `e : p => t`, then `EProofApp e : t`, as long as we can prove p.

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] 

data Match Source

Constructors

From QName Type Expr

do we need this type? it seems like it can be computed from the expr

Let Decl 

data DeclGroup Source

Constructors

Recursive [Decl]

Mutually recursive declarations

NonRecursive Decl

Non-recursive declaration

tNum :: Integral a => a -> Type Source

eError :: Type -> String -> Expr Source

Make an expression that is error pre-applied to a type and a message.

tRec :: [(Name, Type)] -> Type Source

tFun :: Type -> Type -> Type infixr 5 Source

Make a function type.

tNoUser :: Type -> Type Source

Eliminate type synonyms.

(=#=) :: Type -> Type -> Prop infix 4 Source

Equality for numeric types.

(>==) :: Type -> Type -> Prop infix 4 Source

Make a greater-than-or-equal-to constraint.

pHas :: Selector -> Type -> Type -> Prop Source

A Has constraint, used for tuple and record selection.

(.*.) :: Type -> Type -> Type infixl 7 Source

Make multiplication type.

(.+.) :: Type -> Type -> Type infixl 6 Source

Make addition type.

tMin :: Type -> Type -> Type Source

Make a min type.

quickApply :: Kind -> [a] -> Kind Source

ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(QName, Type)] -> Expr -> Doc Source

splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source

data TFun 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
TCLg2
 : Num -> Num
TCExp
 : Num -> Num -> Num
TCWidth
 : Num -> Num
TCMin
 : Num -> Num -> Num
TCMax
 : Num -> Num -> Num
TCLenFromThen

: Num -> Num -> Num -> Num Example: [ 1, 5 .. ] :: [lengthFromThen 1 5 b][b]

TCLenFromThenTo

: Num -> Num -> Num -> Num Example: [ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]

newtype ModName Source

Module names are just namespaces.

INVARIANT: the list of strings should never be empty in a valid module name.

Constructors

ModName [String] 

data Selector Source

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 Name (Maybe [Name])

Record selection. Optionally specifies the shape of the record.

ListSel Int (Maybe Int)

List selection. Optionally specifies the length of the list.

data Import Source

An import declaration.

Constructors

Import 

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.

Constructors

Hiding [Name] 
Only [Name] 

data ExportType Source

Export information for a declaration.

Constructors

Public 
Private 

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.