why3-0.8: Haskell support for the Why3 input format.

Safe HaskellTrustworthy
LanguageHaskell98

Language.Why3.Lexer

Documentation

primLexer :: ByteString -> [Token] Source

lexer :: ByteString -> [Token] Source

data Token Source

Constructors

Token 

Fields

tokenType :: TokenT
 
tokenText :: Text
 
tokenPos :: Position
 

Instances

data TokenT Source

Constructors

Num Integer Int

value, base

RealTok

We don't process reals for now

Ident IdQual IdCase

qualified?, classification

TIdent

Theory identifier

StrLit Text

string literal

KW TokenKW

keyword

Sym TokenSym

symbols

Op TokenOp

operators

White TokenW

white space token

Err TokenErr

error token

EOF

End of file

Instances

data IdQual Source

Constructors

Unqual 
Qual 

Instances

data IdCase Source

Constructors

Lower 
Upper 

Instances

data TokenKW Source

Constructors

KW_if 
KW_then 
KW_else 
KW_let 
KW_in 
KW_match 
KW_with 
KW_end 
KW_as 
KW_forall 
KW_exists 
KW_not 
KW_true 
KW_false 
KW_theory 
KW_type 
KW_constant 
KW_function 
KW_predicate 
KW_inductive 
KW_coinductive 
KW_axiom 
KW_lemma 
KW_goal 
KW_use 
KW_clone 
KW_namespace 
KW_import 
KW_export 

Instances

data TokenErr Source

Constructors

UnterminatedComment 
UnterminatedString 
UnterminatedChar 
InvalidString 
InvalidChar 
LexicalError 

Instances

data TokenOp Source

Constructors

ArrowL 
ArrowR 
ArrowLR 
AsymDisj 
Disj 
AsymConj 
Conj 
BangOp 
OtherOp Int 

Instances

data TokenSym Source

Constructors

Comma 
Dot 
Semi 
Colon 
Quote 
Eq 
Underscore 
Bar 
ParenL 
ParenR 
BracketL 
BracketR 
CurlyL 
CurlyR 

Instances

data TokenW Source

Constructors

BlockComment 
Space 

Instances

data Position Source

Constructors

Position 

Fields

line :: !Int
 
col :: !Int
 

Instances