cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.AST

Description

Synopsis

- data Module = Module {
  - mName :: ModName
  - mExports :: ExportSpec
  - mImports :: [Import]
  - mTySyns :: Map QName TySyn
  - mNewtypes :: Map QName Newtype
  - mDecls :: [DeclGroup]
  }
- data Kind
  - = KType
  - | KNum
  - | KProp
  - | Kind :-> Kind
- data Schema = Forall {
  - sVars :: [TParam]
  - sProps :: [Prop]
  - sType :: Type
  }
- data TySyn = TySyn {
  - tsName :: QName
  - tsParams :: [TParam]
  - tsConstraints :: [Prop]
  - tsDef :: Type
  }
- data Newtype = Newtype {
  - ntName :: QName
  - ntParams :: [TParam]
  - ntConstraints :: [Prop]
  - ntFields :: [(Name, Type)]
  }
- data TParam = TParam {
  - tpUnique :: !Int
  - tpKind :: Kind
  - tpName :: Maybe QName
  }
- tpVar :: TParam -> TVar
- data Type
  - = TCon TCon [Type]
  - | TVar TVar
  - | TUser QName [Type] Type
  - | TRec [(Name, Type)]
- type Prop = Type
- type SType = Type
- data TVar
  - = TVFree !Int Kind (Set TVar) Doc
  - | TVBound !Int Kind
- data TCon
  - = TC TC
  - | PC PC
  - | TF TFun
- data PC
  - = PEqual
  - | PNeq
  - | PGeq
  - | PFin
  - | PHas Selector
  - | PArith
  - | PCmp
- data TC
  - = TCNum Integer
  - | TCInf
  - | TCBit
  - | TCSeq
  - | TCFun
  - | TCTuple Int
  - | TCNewtype UserTC
- data UserTC = UserTC QName Kind
- data Expr
  - = ECon ECon
  - | EList [Expr] Type
  - | ETuple [Expr]
  - | ERec [(Name, Expr)]
  - | ESel Expr Selector
  - | EIf Expr Expr Expr
  - | EComp Type Expr [[Match]]
  - | EVar QName
  - | ETAbs TParam Expr
  - | ETApp Expr Type
  - | EApp Expr Expr
  - | EAbs QName Type Expr
  - | EProofAbs Prop Expr
  - | EProofApp Expr
  - | ECast Expr Type
  - | EWhere Expr [DeclGroup]
- data Match
  - = From QName Type Expr
  - | Let Decl
- 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
  - kindOf :: t -> Kind
- 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
  - = TCAdd
  - | TCSub
  - | TCMul
  - | TCDiv
  - | TCMod
  - | TCLg2
  - | TCExp
  - | TCWidth
  - | TCMin
  - | TCMax
  - | TCLenFromThen
  - | TCLenFromThenTo
- data Name
  - = Name String
  - | NewName Pass Int
- data QName = QName (Maybe ModName) Name
- mkUnqual :: Name -> QName
- unqual :: QName -> Name
- newtype ModName = ModName [String]
- data Selector
  - = TupleSel Int (Maybe Int)
  - | RecordSel Name (Maybe [Name])
  - | ListSel Int (Maybe Int)
- data Import = Import {
  - iModule :: ModName
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  }
- data ImportSpec
  - = Hiding [Name]
  - | Only [Name]
- data ExportType
  - = Public
  - | Private
- data ExportSpec = ExportSpec {
  - eTypes :: Set QName
  - eBinds :: Set QName
  }
- isExportedBind :: QName -> ExportSpec -> Bool
- isExportedType :: QName -> ExportSpec -> Bool
- data Pragma
  - = PragmaNote String
  - | PragmaProperty

# Documentation

data Module Source

A Cryptol module.

Constructors

Module |

Fields

mName :: ModName
mExports :: ExportSpec
mImports :: [Import]
mTySyns :: Map QName TySyn
mNewtypes :: Map QName Newtype
mDecls :: [DeclGroup]

Instances

Show Module Source |
PP Module Source |
TVars Module Source |
PP (WithNames Module) Source |

data Kind Source

Kinds, classify types.

Constructors

KType |
KNum |
KProp |
Kind :-> Kind infixr 5 |

Instances

Eq Kind Source |
Show Kind Source |
PP Kind Source |

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

Instances

Eq TySyn Source |
Show TySyn Source |
PP TySyn Source |
HasKind TySyn Source |
PP (WithNames TySyn) Source |

data Newtype Source

Named records

Constructors

Newtype |

Fields

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

Instances

Show Newtype Source |
HasKind Newtype Source |

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.

Instances

Eq TParam Source |
Ord TParam Source |
Show TParam Source |
PP TParam Source |
HasKind TParam Source |
PP (WithNames TParam) Source |

tpVar :: TParam -> TVar Source

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

Instances

Eq Type Source |
Ord Type Source |
Show Type Source |
PP Type Source |
HasKind Type Source |
TVars Type Source |
FVS Type Source |
IsFact Prop Source |
TrieMap TypeMap Type Source |
PP (WithNames Type) Source |

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 |

Instances

Eq TVar Source |
Ord TVar Source |
Show TVar Source |
HasKind TVar Source |
PP (WithNames TVar) Source |

data TCon Source

Type constants.

Constructors

TC TC |
PC PC |
TF TFun |

Instances

Eq TCon Source |
Ord TCon Source |
Show TCon Source |
PP TCon Source |
HasKind TCon Source |

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 _

Instances

Eq PC Source |
Ord PC Source |
Show PC Source |
PP PC Source |
HasKind PC Source |

data TC Source

1-1 constants.

Constructors

TCNum Integer | Numbers
TCInf | Inf
TCBit | Bit

TCSeq

    [_] _

TCFun

    _ -> _

TCTuple Int

    (_, _, _)

TCNewtype UserTC | user-defined, `T`

Instances

Eq TC Source |
Ord TC Source |
Show TC Source |
PP TC Source |
HasKind TC Source |

data UserTC Source

Constructors

UserTC QName Kind |

Instances

Eq UserTC Source |
Ord UserTC Source |
Show UserTC Source |
PP UserTC Source |
HasKind UserTC Source |

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] |

Instances

Show Expr Source |
PP Expr Source |
TVars Expr Source |
PP (WithNames Expr) Source |

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 |

Instances

Show Match Source |
PP Match Source |
TVars Match Source |
PP (WithNames Match) Source |

data DeclGroup Source

Constructors

Recursive [Decl] | Mutually recursive declarations
NonRecursive Decl | Non-recursive declaration

Instances

Show DeclGroup Source |
PP DeclGroup Source |
TVars DeclGroup Source |
PP (WithNames DeclGroup) Source |

groupDecls :: DeclGroup -> [Decl] Source

data Decl Source

Constructors

Decl |

Fields

dName :: QName
dSignature :: Schema
dDefinition :: Expr
dPragmas :: [Pragma]

Instances

Show Decl Source |
PP Decl Source |
TVars Decl Source |
PP (WithNames Decl) Source |

isFreeTV :: TVar -> Bool Source

isBoundTV :: TVar -> Bool Source

tIsNum :: Type -> Maybe Integer Source

tIsInf :: Type -> Bool Source

tIsVar :: Type -> Maybe TVar Source

tIsFun :: Type -> Maybe (Type, Type) Source

tIsSeq :: Type -> Maybe (Type, Type) Source

tIsBit :: Type -> Bool Source

tIsTuple :: Type -> Maybe [Type] Source

pIsFin :: Prop -> Maybe Type Source

pIsGeq :: Prop -> Maybe (Type, Type) Source

pIsEq :: Prop -> Maybe (Type, Type) Source

pIsArith :: Prop -> Maybe Type Source

pIsCmp :: Prop -> Maybe Type Source

pIsNumeric :: Prop -> Bool Source

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

tZero :: Type Source

tOne :: Type Source

tTwo :: Type Source

tInf :: Type Source

tBit :: Type Source

eTrue :: Expr Source

eFalse :: Expr Source

tWord :: Type -> Type Source

tSeq :: Type -> Type -> Type Source

tChar :: Type Source

eChar :: Char -> Expr Source

tString :: Int -> Type Source

eString :: String -> Expr 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

tTuple :: [Type] -> Type Source

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

Make a function type.

tNoUser :: Type -> Type Source

Eliminate type synonyms.

tWidth :: Type -> Type Source

tLenFromThen :: Type -> Type -> Type -> Type Source

tLenFromThenTo :: Type -> Type -> Type -> Type Source

tMax :: Type -> Type -> Type Source

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

Equality for numeric types.

(=/=) :: Type -> Type -> Prop Source

pArith :: Type -> Prop Source

pCmp :: Type -> Prop Source

(>==) :: 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.

pFin :: Type -> Prop Source

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

Make multiplication type.

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

Make addition type.

(.-.) :: Type -> Type -> Type Source

(.^.) :: Type -> Type -> Type Source

tDiv :: Type -> Type -> Type Source

tMod :: Type -> Type -> Type Source

tMin :: Type -> Type -> Type Source

Make a `min` type.

newtypeTyCon :: Newtype -> TCon Source

newtypeConType :: Newtype -> Schema Source

class HasKind t where Source

Methods

kindOf :: t -> Kind Source

Instances

HasKind TFun Source |
HasKind UserTC Source |
HasKind TC Source |
HasKind PC Source |
HasKind TCon Source |
HasKind TVar Source |
HasKind Type Source |
HasKind TParam Source |
HasKind Newtype Source |
HasKind TySyn Source |

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

addTNames :: [TParam] -> NameMap -> NameMap Source

ppNewtypeShort :: Newtype -> Doc Source

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

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

splitAbs :: Expr -> Maybe ((QName, Type), Expr) Source

splitTAbs :: Expr -> Maybe (TParam, Expr) Source

splitProofAbs :: Expr -> Maybe (Prop, Expr) 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]`

Instances

Bounded TFun Source |
Enum TFun Source |
Eq TFun Source |
Ord TFun Source |
Show TFun Source |
PP TFun Source |
HasKind TFun Source |

data Name Source

Constructors

Name String |
NewName Pass Int |

Instances

Eq Name Source |
Ord Name Source |
Show Name Source |
PP Name Source |

data QName Source

Constructors

QName (Maybe ModName) Name |

Instances

Eq QName Source |
Ord QName Source |
Show QName Source |
PP QName Source |

mkUnqual :: Name -> QName Source

unqual :: QName -> Name Source

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] |

Instances

Eq ModName Source |
Ord ModName Source |
Show ModName Source |
PP ModName Source |

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.

Instances

Eq Selector Source |
Ord Selector Source |
Show Selector Source |
PP Selector Source |

data Import Source

An import declaration.

Constructors

Import |

Fields

iModule :: ModName
iAs :: Maybe ModName
iSpec :: Maybe ImportSpec

Instances

Eq Import Source |
Show Import Source |
PP Import Source |

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] |

Instances

Eq ImportSpec Source |
Show ImportSpec Source |
PP ImportSpec Source |

data ExportType Source

Export information for a declaration.

Constructors

Public |
Private |

Instances

Eq ExportType Source |
Ord ExportType Source |
Show ExportType Source |

data ExportSpec Source

Constructors

ExportSpec |

Fields

eTypes :: Set QName
eBinds :: Set QName

Instances

Show ExportSpec Source |
Monoid 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.

data Pragma Source

Constructors

PragmaNote String |
PragmaProperty |

Instances

Eq Pragma Source |
Show Pragma Source |
PP Pragma Source |
NoPos Pragma Source |
Rename Pragma Source |