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

Contents

- Names
- Types
- Declarations
- Interactive
- Expressions
- Positions
- Pretty-printing

Description

Synopsis

- newtype ModName = ModName [String]
- modRange :: Module -> Range
- data QName = QName (Maybe ModName) Name
- mkQual :: ModName -> Name -> QName
- mkUnqual :: Name -> QName
- unqual :: QName -> Name
- data Name
  - = Name String
  - | NewName Pass Int
- data Named a = Named {
  - name :: Located Name
  - value :: a
  }
- data Pass
  - = NoPat
  - | MonoValues
- data Schema = Forall [TParam] [Prop] Type (Maybe Range)
- data TParam = TParam {
  - tpName :: Name
  - tpKind :: Maybe Kind
  - tpRange :: Maybe Range
  }
- tpQName :: TParam -> QName
- data Kind
  - = KNum
  - | KType
- data Type
  - = TFun Type Type
  - | TSeq Type Type
  - | TBit
  - | TNum Integer
  - | TChar Char
  - | TInf
  - | TUser QName [Type]
  - | TApp TFun [Type]
  - | TRecord [Named Type]
  - | TTuple [Type]
  - | TWild
  - | TLocated Type Range
- data Prop
  - = CFin Type
  - | CEqual Type Type
  - | CGeq Type Type
  - | CArith Type
  - | CCmp Type
  - | CLocated Prop Range
- data Module = Module {
  - mName :: Located ModName
  - mImports :: [Located Import]
  - mDecls :: [TopDecl]
  }
- newtype Program = Program [TopDecl]
- data TopDecl
  - = Decl (TopLevel Decl)
  - | TDNewtype (TopLevel Newtype)
  - | Include (Located FilePath)
- data Decl
  - = DSignature [LQName] Schema
  - | DPragma [LQName] Pragma
  - | DBind Bind
  - | DPatBind Pattern Expr
  - | DType TySyn
  - | DLocated Decl Range
- data TySyn = TySyn LQName [TParam] Type
- data Bind = Bind {
  - bName :: LQName
  - bParams :: [Pattern]
  - bDef :: Expr
  - bSignature :: Maybe Schema
  - bPragmas :: [Pragma]
  - bMono :: Bool
  }
- data Pragma
  - = PragmaNote String
  - | PragmaProperty
- data ExportType
  - = Public
  - | Private
- data ExportSpec = ExportSpec {
  - eTypes :: Set QName
  - eBinds :: Set QName
  }
- exportBind :: TopLevel QName -> ExportSpec
- exportType :: TopLevel QName -> ExportSpec
- isExportedBind :: QName -> ExportSpec -> Bool
- isExportedType :: QName -> ExportSpec -> Bool
- data TopLevel a = TopLevel {
  - tlExport :: ExportType
  - tlValue :: a
  }
- data Import = Import {
  - iModule :: ModName
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  }
- data ImportSpec
  - = Hiding [Name]
  - | Only [Name]
- data Newtype = Newtype {
  - nName :: LQName
  - nParams :: [TParam]
  - nBody :: [Named Type]
  }
- data ReplInput
  - = ExprInput Expr
  - | LetInput Decl
- data Expr
  - = EVar QName
  - | ECon ECon
  - | ELit Literal
  - | ETuple [Expr]
  - | ERecord [Named Expr]
  - | ESel Expr Selector
  - | EList [Expr]
  - | EFromTo Type (Maybe Type) (Maybe Type)
  - | EInfFrom Expr (Maybe Expr)
  - | EComp Expr [[Match]]
  - | EApp Expr Expr
  - | EAppT Expr [TypeInst]
  - | EIf Expr Expr Expr
  - | EWhere Expr [Decl]
  - | ETyped Expr Type
  - | ETypeVal Type
  - | EFun [Pattern] Expr
  - | ELocated Expr Range
- data Literal
  - = ECNum Integer NumInfo
  - | ECString String
- data NumInfo
  - = BinLit Int
  - | OctLit Int
  - | DecLit
  - | HexLit Int
  - | CharLit
  - | PolyLit Int
- data Match
  - = Match Pattern Expr
  - | MatchLet Bind
- data Pattern
  - = PVar LName
  - | PWild
  - | PTuple [Pattern]
  - | PRecord [Named Pattern]
  - | PList [Pattern]
  - | PTyped Pattern Type
  - | PSplit Pattern Pattern
  - | PLocated Pattern Range
- data Selector
  - = TupleSel Int (Maybe Int)
  - | RecordSel Name (Maybe [Name])
  - | ListSel Int (Maybe Int)
- data TypeInst
  - = NamedInst (Named Type)
  - | PosInst Type
- data Located a = Located {
  - srcRange :: !Range
  - thing :: a
  }
- type LName = Located Name
- type LQName = Located QName
- type LString = Located String
- class NoPos t where
  - noPos :: t -> t
- cppKind :: Kind -> Doc
- ppSelector :: Selector -> Doc

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

Instances

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

modRange :: Module -> Range Source

data QName Source

Constructors

QName (Maybe ModName) Name |

Instances

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

mkQual :: ModName -> Name -> QName Source

mkUnqual :: Name -> QName Source

unqual :: QName -> Name Source

data Name Source

Constructors

Name String |
NewName Pass Int |

Instances

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

data Named a Source

Constructors

Named |

Fields

name :: Located Name
value :: a

Instances

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

data Pass Source

Constructors

NoPat |
MonoValues |

Instances

Eq Pass Source |
Ord Pass Source |
Show Pass Source |

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

Fields

tpName :: Name
tpKind :: Maybe Kind
tpRange :: Maybe Range

Instances

Eq TParam Source |
Show TParam Source |
PP TParam Source |
AddLoc TParam Source |
HasLoc TParam Source |
NoPos TParam Source |
BindsNames TParam Source | Generate the naming environment for a type parameter.

tpQName :: TParam -> QName Source

data Kind Source

Constructors

KNum |
KType |

Instances

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

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

Instances

Eq Type Source |
Show Type Source |
PP Type Source |
AddLoc Type Source |
HasLoc Type Source |
NoPos Type Source |
Rename Type Source |

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

Instances

Eq Prop Source |
Show Prop Source |
PP Prop Source |
AddLoc Prop Source |
HasLoc Prop Source |
NoPos Prop Source |
Rename Prop Source |

# Declarations

data Module Source

Constructors

Module |

Fields

mName :: Located ModName
mImports :: [Located Import]
mDecls :: [TopDecl]

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 |

newtype Program Source

Constructors

Program [TopDecl] |

Instances

Eq Program Source |
Show Program Source |
PP Program Source |
NoPos Program Source |
RemovePatterns Program Source |

data TopDecl Source

Constructors

Decl (TopLevel Decl) |
TDNewtype (TopLevel Newtype) |
Include (Located FilePath) |

Instances

Eq TopDecl Source |
Show TopDecl Source |
PP TopDecl Source |
HasLoc TopDecl Source |
NoPos TopDecl Source |
Rename TopDecl Source |
FromDecl TopDecl Source |

data Decl Source

Constructors

DSignature [LQName] Schema |
DPragma [LQName] Pragma |
DBind Bind |
DPatBind Pattern Expr |
DType TySyn |
DLocated Decl Range |

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

Constructors

TySyn LQName [TParam] Type |

Instances

Eq TySyn Source |
Show TySyn Source |
PP TySyn Source |
NoPos TySyn Source |
Rename TySyn 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 Pragma Source

Constructors

PragmaNote String |
PragmaProperty |

Instances

Eq Pragma Source |
Show Pragma Source |
PP Pragma Source |
NoPos Pragma Source |
Rename Pragma 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 |

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 Source |
Eq a => Eq (TopLevel a) Source |
Ord a => Ord (TopLevel a) Source |
Show a => Show (TopLevel a) Source |
PP a => PP (TopLevel a) Source |
HasLoc a => HasLoc (TopLevel a) Source |
NoPos a => NoPos (TopLevel a) Source |
Rename a => Rename (TopLevel a) 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 Newtype Source

Constructors

Newtype |

Fields

nName :: LQName

  Type name

nParams :: [TParam]

  Type params

nBody :: [Named Type]

  Constructor

Instances

Eq Newtype Source |
Show Newtype Source |
PP Newtype Source |
HasLoc Newtype Source |
NoPos Newtype Source |
Rename Newtype Source |

# Interactive

data ReplInput Source

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

Constructors

ExprInput Expr |
LetInput Decl |

Instances

Eq ReplInput Source |
Show ReplInput Source |

# 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

Instances

Eq Expr Source |
Show Expr Source |
PP Expr Source |
AddLoc Expr Source |
HasLoc Expr Source |
NoPos Expr Source |
RemovePatterns Expr Source |
Rename Expr Source |

data Literal Source

Literals.

Constructors

ECNum Integer NumInfo | `0x10` (HexLit 2)

ECString String

    "hello"

Instances

Eq Literal Source |
Show Literal Source |
PP Literal Source |

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

Eq NumInfo Source |
Show NumInfo Source |

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.

Instances

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

data TypeInst Source

Constructors

NamedInst (Named Type) |
PosInst Type |

Instances

Eq TypeInst Source |
Show TypeInst Source |
PP TypeInst Source |
NoPos TypeInst Source |
Rename TypeInst Source |

# Positions

data Located a Source

Constructors

Located |

Fields

srcRange :: !Range
thing :: a

Instances

Functor Located Source |
Eq a => Eq (Located a) Source |
Show a => Show (Located a) Source |
PP a => PP (Located a) Source |
AddLoc (Located a) Source |
HasLoc (Located a) Source |
NoPos (Located t) Source |
Rename a => Rename (Located a) Source |

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.

class NoPos t where Source

Methods

noPos :: t -> t Source

Instances

NoPos Prop Source |
NoPos Type Source |
NoPos TParam Source |
NoPos Schema Source |
NoPos Pattern Source |
NoPos Match Source |
NoPos TypeInst Source |
NoPos Expr Source |
NoPos Newtype Source |
NoPos Pragma Source |
NoPos Bind Source |
NoPos TySyn Source |
NoPos Decl Source |
NoPos TopDecl Source |
NoPos Module Source |
NoPos Program Source |
NoPos t => NoPos [t] Source |
NoPos t => NoPos (Maybe t) Source |
NoPos (Located t) Source |
NoPos t => NoPos (Named t) Source |
NoPos a => NoPos (TopLevel a) Source |

# 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.