snappea 0.1.0

//! Tokens of the P language.

use crate::syntax::span::Span;

/// Kinds of tokens produced by the lexer. Keyword tokens mirror `PLexer.g4` upstream.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum TokenKind {
    // type names
    Any,
    Bool,
    Enum,
    Event,
    EventSet,
    Float,
    Int,
    Machine,
    Interface,
    Map,
    Set,
    String,
    Seq,
    Data,
    // keywords
    Announce,
    As,
    Assert,
    Break,
    Case,
    Cold,
    Continue,
    Default,
    Defer,
    Do,
    Else,
    Entry,
    Exit,
    Foreach,
    Format,
    Fun,
    Goto,
    Halt,
    Hot,
    If,
    Ignore,
    In,
    Keys,
    New,
    Observes,
    On,
    Print,
    Raise,
    Receive,
    Return,
    Scenario,
    Send,
    Sizeof,
    Spec,
    Start,
    State,
    This,
    Type,
    Values,
    Var,
    Param,
    Pairwise,
    Wise,
    While,
    With,
    Choose,
    // verifier keywords
    Invariant,
    Axiom,
    Is,
    Inflight,
    Targets,
    Sent,
    Proof,
    Prove,
    Using,
    Lemma,
    Theorem,
    Except,
    Requires,
    Ensures,
    Forall,
    Exists,
    InitCondition,
    Pure,
    Assume,
    // module system
    Module,
    Implementation,
    Test,
    ParamTest,
    Refines,
    Compose,
    Union,
    HideE,
    HideI,
    Rename,
    Safe,
    Main,
    Receives,
    Sends,
    Creates,
    To,
    // literals
    BoolLiteral,
    IntLiteral,
    NullLiteral,
    StringLiteral,
    // symbols
    FairNondet,
    Nondet,
    LNot,
    LAnd,
    LOr,
    LThen,
    LIff,
    Eq,
    Ne,
    Le,
    Ge,
    Lt,
    Gt,
    RArrow,
    Assign,
    Insert,
    Remove,
    Add,
    Sub,
    Mul,
    Div,
    Mod,
    LBrace,
    RBrace,
    LBrack,
    RBrack,
    LParen,
    RParen,
    Semi,
    Comma,
    Dot,
    Colon,
    Iden,
    Eof,
}

impl TokenKind {
    /// Human readable, upstream-style display name used in parse error messages.
    pub fn display(self) -> &'static str {
        use TokenKind::*;
        match self {
            Any => "'any'",
            Bool => "'bool'",
            Enum => "'enum'",
            Event => "'event'",
            EventSet => "'eventset'",
            Float => "'float'",
            Int => "'int'",
            Machine => "'machine'",
            Interface => "'interface'",
            Map => "'map'",
            Set => "'set'",
            String => "'string'",
            Seq => "'seq'",
            Data => "'data'",
            Announce => "'announce'",
            As => "'as'",
            Assert => "'assert'",
            Break => "'break'",
            Case => "'case'",
            Cold => "'cold'",
            Continue => "'continue'",
            Default => "'default'",
            Defer => "'defer'",
            Do => "'do'",
            Else => "'else'",
            Entry => "'entry'",
            Exit => "'exit'",
            Foreach => "'foreach'",
            Format => "'format'",
            Fun => "'fun'",
            Goto => "'goto'",
            Halt => "'halt'",
            Hot => "'hot'",
            If => "'if'",
            Ignore => "'ignore'",
            In => "'in'",
            Keys => "'keys'",
            New => "'new'",
            Observes => "'observes'",
            On => "'on'",
            Print => "'print'",
            Raise => "'raise'",
            Receive => "'receive'",
            Return => "'return'",
            Scenario => "'scenario'",
            Send => "'send'",
            Sizeof => "'sizeof'",
            Spec => "'spec'",
            Start => "'start'",
            State => "'state'",
            This => "'this'",
            Type => "'type'",
            Values => "'values'",
            Var => "'var'",
            Param => "'param'",
            Pairwise => "'pairwise'",
            Wise => "'wise'",
            While => "'while'",
            With => "'with'",
            Choose => "'choose'",
            Invariant => "'invariant'",
            Axiom => "'axiom'",
            Is => "'is'",
            Inflight => "'inflight'",
            Targets => "'targets'",
            Sent => "'sent'",
            Proof => "'Proof'",
            Prove => "'prove'",
            Using => "'using'",
            Lemma => "'Lemma'",
            Theorem => "'Theorem'",
            Except => "'except'",
            Requires => "'requires'",
            Ensures => "'ensures'",
            Forall => "'forall'",
            Exists => "'exists'",
            InitCondition => "'init-condition'",
            Pure => "'pure'",
            Assume => "'assume'",
            Module => "'module'",
            Implementation => "'implementation'",
            Test => "'test'",
            ParamTest => "'paramtest'",
            Refines => "'refines'",
            Compose => "'compose'",
            Union => "'union'",
            HideE => "'hidee'",
            HideI => "'hidei'",
            Rename => "'rename'",
            Safe => "'safe'",
            Main => "'main'",
            Receives => "'receives'",
            Sends => "'sends'",
            Creates => "'creates'",
            To => "'to'",
            BoolLiteral => "BoolLiteral",
            IntLiteral => "IntLiteral",
            NullLiteral => "'null'",
            StringLiteral => "StringLiteral",
            FairNondet => "'$$'",
            Nondet => "'$'",
            LNot => "'!'",
            LAnd => "'&&'",
            LOr => "'||'",
            LThen => "'==>'",
            LIff => "'<==>'",
            Eq => "'=='",
            Ne => "'!='",
            Le => "'<='",
            Ge => "'>='",
            Lt => "'<'",
            Gt => "'>'",
            RArrow => "'->'",
            Assign => "'='",
            Insert => "'+='",
            Remove => "'-='",
            Add => "'+'",
            Sub => "'-'",
            Mul => "'*'",
            Div => "'/'",
            Mod => "'%'",
            LBrace => "'{'",
            RBrace => "'}'",
            LBrack => "'['",
            RBrack => "']'",
            LParen => "'('",
            RParen => "')'",
            Semi => "';'",
            Comma => "','",
            Dot => "'.'",
            Colon => "':'",
            Iden => "Iden",
            Eof => "<EOF>",
        }
    }

    /// Returns the keyword kind for an identifier-like word, if it is a keyword.
    pub fn keyword(word: &str) -> Option<TokenKind> {
        use TokenKind::*;
        Some(match word {
            "any" => Any,
            "bool" => Bool,
            "enum" => Enum,
            "event" => Event,
            "eventset" => EventSet,
            "float" => Float,
            "int" => Int,
            "machine" => Machine,
            "interface" => Interface,
            "map" => Map,
            "set" => Set,
            "string" => String,
            "seq" => Seq,
            "data" => Data,
            "announce" => Announce,
            "as" => As,
            "assert" => Assert,
            "break" => Break,
            "case" => Case,
            "cold" => Cold,
            "continue" => Continue,
            "default" => Default,
            "defer" => Defer,
            "do" => Do,
            "else" => Else,
            "entry" => Entry,
            "exit" => Exit,
            "foreach" => Foreach,
            "format" => Format,
            "fun" => Fun,
            "goto" => Goto,
            "halt" => Halt,
            "hot" => Hot,
            "if" => If,
            "ignore" => Ignore,
            "in" => In,
            "keys" => Keys,
            "new" => New,
            "observes" => Observes,
            "on" => On,
            "print" => Print,
            "raise" => Raise,
            "receive" => Receive,
            "return" => Return,
            "scenario" => Scenario,
            "send" => Send,
            "sizeof" => Sizeof,
            "spec" => Spec,
            "start" => Start,
            "state" => State,
            "this" => This,
            "type" => Type,
            "values" => Values,
            "var" => Var,
            "param" => Param,
            "pairwise" => Pairwise,
            "wise" => Wise,
            "while" => While,
            "with" => With,
            "choose" => Choose,
            "invariant" => Invariant,
            "axiom" => Axiom,
            "is" => Is,
            "inflight" => Inflight,
            "targets" => Targets,
            "sent" => Sent,
            "Proof" => Proof,
            "prove" => Prove,
            "using" => Using,
            "Lemma" => Lemma,
            "Theorem" => Theorem,
            "except" => Except,
            "requires" => Requires,
            "ensures" => Ensures,
            "forall" => Forall,
            "exists" => Exists,
            "pure" => Pure,
            "assume" => Assume,
            "module" => Module,
            "implementation" => Implementation,
            "test" => Test,
            "paramtest" => ParamTest,
            "refines" => Refines,
            "compose" => Compose,
            "union" => Union,
            "hidee" => HideE,
            "hidei" => HideI,
            "rename" => Rename,
            "safe" => Safe,
            "main" => Main,
            "receives" => Receives,
            "sends" => Sends,
            "creates" => Creates,
            "to" => To,
            "true" | "false" => BoolLiteral,
            "null" => NullLiteral,
            _ => return None,
        })
    }

    /// True for the keywords that only the PVerifier backend accepts.
    pub fn is_verifier_only(self) -> bool {
        use TokenKind::*;
        matches!(
            self,
            Invariant
                | Axiom
                | Is
                | Inflight
                | Targets
                | Sent
                | Proof
                | Prove
                | Using
                | Lemma
                | Theorem
                | Except
                | Requires
                | Ensures
                | Forall
                | Exists
                | InitCondition
                | Pure
        )
    }
}

/// A lexed token with its source span.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Token {
    pub kind: TokenKind,
    pub span: Span,
}