cryptol-2.2.2: 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 QName Source

Constructors

QName (Maybe ModName) Name 

Instances

data Name Source

Constructors

Name String 
NewName Pass Int 

Instances

data Named a Source

Constructors

Named 

Fields

name :: Located Name
 
value :: a
 

Instances

Functor Named 
Eq a => Eq (Named a) 
Show a => Show (Named a) 
HasLoc a => HasLoc (Named a) 
NoPos t => NoPos (Named t) 
Rename a => Rename (Named a) 

data Pass Source

Constructors

NoPat 
MonoValues 

Instances

Types

data Schema Source

Constructors

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

Instances

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

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

Rename Schema

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

data TParam Source

Constructors

TParam 

Instances

Eq TParam 
Show TParam 
PP TParam 
AddLoc TParam 
HasLoc TParam 
NoPos TParam 
BindsNames TParam

Generate the naming environment for a type parameter.

data Kind Source

Constructors

KNum 
KType 

Instances

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 
Show Module 
PP Module 
HasLoc Module 
NoPos Module 
BindsNames Module

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

RemovePatterns Module 
Rename Module 

data Decl Source

Instances

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

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

Rename Decl 
FromDecl Decl 
RemovePatterns [Decl] 

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 
Show Bind 
PP Bind 
HasLoc Bind 
NoPos Bind 
BindsNames Bind 
Rename Bind

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
 

Instances

Functor TopLevel 
Eq a => Eq (TopLevel a) 
Ord a => Ord (TopLevel a) 
Show a => Show (TopLevel a) 
PP a => PP (TopLevel a) 
HasLoc a => HasLoc (TopLevel a) 
NoPos a => NoPos (TopLevel a) 
Rename a => Rename (TopLevel a) 

data Import Source

An import declaration.

Constructors

Import 

Instances

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 Newtype Source

Constructors

Newtype 

Fields

nName :: LQName

Type name

nParams :: [TParam]

Type params

nBody :: [Named Type]

Constructor

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

Instances

data Match Source

Constructors

Match Pattern Expr

p <- e

MatchLet Bind 

Instances

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

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

Rename Match 

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 
Show Pattern 
PP Pattern 
AddLoc Pattern 
HasLoc Pattern 
NoPos Pattern 
BindsNames Pattern

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

Rename Pattern 

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
 

Instances

Functor Located 
Eq a => Eq (Located a) 
Show a => Show (Located a) 
PP a => PP (Located a) 
AddLoc (Located a) 
HasLoc (Located a) 
NoPos (Located t) 
Rename a => Rename (Located 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.