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.Parser.AST

Contents

Description

 

Synopsis

Names

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 Named a Source

Constructors

Named 

Fields

name :: Located Name
 
value :: a
 

Instances

data Pass Source

Constructors

NoPat 
MonoValues 

Types

data Schema Source

Constructors

Forall [TParam] [Prop] Type (Maybe Range) 

Instances

Eq Schema Source 
Show Schema Source 
PP Schema Source 
AddLoc Schema Source 
HasLoc Schema Source 
NoPos Schema Source 
BindsNames Schema Source

Generate a type renaming environment from the parameters that are bound by this schema.

Rename Schema Source

Rename a schema, assuming that none of its type variables are already in scope.

data TParam Source

Constructors

TParam 

Instances

data Kind Source

Constructors

KNum 
KType 

data Type Source

Constructors

TFun Type Type
[8] -> [8]
TSeq Type Type
[8] a
TBit
Bit
TNum Integer
10
TChar Char
a
TInf
inf
TUser QName [Type]

A type variable or synonym

TApp TFun [Type]
2 + x
TRecord [Named Type]
{ x : [8], y : [32] }
TTuple [Type]
([8], [32])
TWild

_, just some type.

TLocated Type Range

Location information

data Prop Source

Constructors

CFin Type
 fin x
CEqual Type Type
 x == 10
CGeq Type Type
 x >= 10
CArith Type
 Arith a
CCmp Type
 Cmp a
CLocated Prop Range

Location information

Declarations

data Module Source

Constructors

Module 

Instances

Eq Module Source 
Show Module Source 
PP Module Source 
HasLoc Module Source 
NoPos Module Source 
BindsNames Module Source

The naming environment for a single module. This is the mapping from unqualified internal names to fully qualified names.

RemovePatterns Module Source 
Rename Module Source 

data Decl Source

Instances

Eq Decl Source 
Show Decl Source 
PP Decl Source 
AddLoc Decl Source 
HasLoc Decl Source 
NoPos Decl Source 
BindsNames Decl Source

The naming environment for a single declaration, unqualified. This is meanat to be used for things like where clauses.

Rename Decl Source 
FromDecl Decl Source 
RemovePatterns [Decl] Source 

data Bind Source

Bindings. Notes:

  • The parser does not associate type signatures and pragmas with their bindings: this is done in a separate pass, after de-sugaring pattern bindings. In this way we can associate pragmas and type signatures with the variables defined by pattern bindings as well.
  • Currently, there is no surface syntax for defining monomorphic bindings (i.e., bindings that will not be automatically generalized by the type checker. However, they are useful when de-sugaring patterns.

Constructors

Bind 

Fields

bName :: LQName

Defined thing

bParams :: [Pattern]

Parameters

bDef :: Expr

Definition

bSignature :: Maybe Schema

Optional type sig

bPragmas :: [Pragma]

Optional pragmas

bMono :: Bool

Is this a monomorphic binding

Instances

Eq Bind Source 
Show Bind Source 
PP Bind Source 
HasLoc Bind Source 
NoPos Bind Source 
BindsNames Bind Source 
Rename Bind Source

Rename a binding.

NOTE: this does not bind its own name into the naming context of its body. The assumption here is that this has been done by the enclosing environment, to allow for top-level renaming

data ExportType Source

Export information for a declaration.

Constructors

Public 
Private 

exportBind :: TopLevel QName -> ExportSpec Source

Add a binding name to the export list, if it should be exported.

exportType :: TopLevel QName -> ExportSpec Source

Add a type synonym name to the export list, if it should be exported.

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 TopLevel a Source

Constructors

TopLevel 

Fields

tlExport :: ExportType
 
tlValue :: a
 

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] 

Interactive

data ReplInput Source

Input at the REPL, which can either be an expression or a let statement.

Constructors

ExprInput Expr 
LetInput Decl 

Expressions

data Expr Source

Constructors

EVar QName
 x
ECon ECon
 split
ELit Literal
 0x10
ETuple [Expr]
 (1,2,3)
ERecord [Named Expr]
 { x = 1, y = 2 }
ESel Expr Selector
 e.l
EList [Expr]
 [1,2,3]
EFromTo Type (Maybe Type) (Maybe Type)
[1, 5 ..  117 ]
EInfFrom Expr (Maybe Expr)
 [1, 3 ...]
EComp Expr [[Match]]
 [ 1 | x <- xs ]
EApp Expr Expr
 f x
EAppT Expr [TypeInst]
 f `{x = 8}, f`{8}
EIf Expr Expr Expr
 if ok then e1 else e2
EWhere Expr [Decl]
 1 + x where { x = 2 }
ETyped Expr Type
 1 : [8]
ETypeVal Type

`(x + 1), x is a type

EFun [Pattern] Expr
 \x y -> x
ELocated Expr Range

position annotation

data Literal Source

Literals.

Constructors

ECNum Integer NumInfo

0x10 (HexLit 2)

ECString String
"hello"

data NumInfo Source

Infromation about the representation of a numeric constant.

Constructors

BinLit Int

n-digit binary literal

OctLit Int

n-digit octal literal

DecLit

overloaded decimal literal

HexLit Int

n-digit hex literal

CharLit

character literal

PolyLit Int

polynomial literal

data Match Source

Constructors

Match Pattern Expr

p <- e

MatchLet Bind 

Instances

Eq Match Source 
Show Match Source 
PP Match Source 
HasLoc Match Source 
NoPos Match Source 
BindsNames Match Source

Translate names bound by the patterns of a match into a renaming environment.

Rename Match Source 

data Pattern Source

Constructors

PVar LName
 x
PWild
 _
PTuple [Pattern]
 (x,y,z)
PRecord [Named Pattern]
 { x = (a,b,c), y = z }
PList [Pattern]
 [ x, y, z ]
PTyped Pattern Type
 x : [8]
PSplit Pattern Pattern
 (x # y)
PLocated Pattern Range

Location information

Instances

Eq Pattern Source 
Show Pattern Source 
PP Pattern Source 
AddLoc Pattern Source 
HasLoc Pattern Source 
NoPos Pattern Source 
BindsNames Pattern Source

Generate an expression renaming environment from a pattern. This ignores type parameters that can be bound by the pattern.

Rename Pattern 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.

Positions

data Located a Source

Constructors

Located 

Fields

srcRange :: !Range
 
thing :: a
 

type LName = Located Name Source

A name with location information.

type LQName = Located QName Source

A qualified name with location information.

type LString = Located String Source

A string with location information.

Pretty-printing

cppKind :: Kind -> Doc Source

Conversational printing of kinds (e.g., to use in error messages)

ppSelector :: Selector -> Doc Source

Display the thing selected by the selector, nicely.