Enum dedukti_parse::Token

source · [−]

pub enum Token<S> {
Show 16 variants    Def,
    Thm,
    LBrk,
    RBrk,
    LPar,
    RPar,
    Colon,
    ColonEq,
    Arrow,
    FatArrow,
    LongArrow,
    Comma,
    Dot,
    Symb(Symb<S>),
    Comment(usize),
    Error,
}

Expand description

A token generated by the lexer.

Variants

`Def`

definition

`Thm`

theorem

`LBrk`

opening bracket

`RBrk`

closing bracket

`LPar`

opening parenthesis

`RPar`

closing parenthesis

`Colon`

has type

`ColonEq`

is defined as

`Arrow`

product

`FatArrow`

abstraction

`LongArrow`

rewrites to

`Comma`

separate variables in rewrite rule contexts

`Dot`

terminate command

`Symb(Symb<S>)`

symbol

`Comment(usize)`

unclosed comments (the number indicates how many comments are still open)

`Error`

unrecognised token

Trait Implementations

source

impl<S: Debug> Debug for Token<S>

source

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

source

impl<S: Display> Display for Token<S>

source

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

source

impl<'s> Logos<'s> for Token<&'s str>

type Extras = ()

Associated type Extras for the particular lexer. This can be set using #[logos(extras = MyExtras)] and accessed inside callbacks. Read more

Source type this token can be lexed from. This will default to str, unless one of the defined patterns explicitly uses non-unicode byte values or byte slices, in which case that implementation will use [u8]. Read more

source

const ERROR: Self = Token { /// definition #[token("def")] Def, /// theorem #[token("thm")] Thm, /// opening bracket #[token("[")] LBrk, /// closing bracket #[token("]")] RBrk, /// opening parenthesis #[token("(")] LPar, /// closing parenthesis #[token(")")] RPar, /// has type #[token(":")] Colon, /// is defined as #[token(":=")] ColonEq, /// product #[token("->")] Arrow, /// abstraction #[token("=>")] FatArrow, /// rewrites to #[token("-->")] LongArrow, /// separate variables in rewrite rule contexts #[token(",")] Comma, /// terminate command #[token(".")] Dot, /// symbol #[regex("[a-zA-Z0-9_!?][a-zA-Z0-9_!?']*", symb)] #[token("{|", moustache)] Symb(Symb), /// unclosed comments (the number indicates how many comments are still open) #[token("(;", comment1)] Comment(usize), /// unrecognised token #[regex(r"[ \t\n\f]+", logos::skip)] #[error] Error

~~Helper const of the variant marked as #[error].~~

source
fn lex(lex: &mut Lexer<'s, Self>)

~~The heart of Logos. Called by the Lexer. The implementation for this function is generated by the logos-derive crate. Read more~~

source
fn lexer(source: &'source Self::Source) -> Lexer<'source, Self> where
Self::Extras: Default,

~~Create a new instance of a Lexer that will produce tokens implementing this Logos. Read more~~

source
fn lexer_with_extras(
source: &'source Self::Source,
extras: Self::Extras
) -> Lexer<'source, Self>

~~Create a new instance of a Lexer with the provided Extras that will produce tokens implementing this Logos. Read more~~

source
impl<S: PartialEq> PartialEq<Token<S>> for Token<S>

source
fn eq(&self, other: &Token<S>) -> bool

~~This method tests for self and other values to be equal, and is used by ==. Read more~~

source
fn ne(&self, other: &Token<S>) -> bool

~~This method tests for !=.~~

source
impl<S: Eq> Eq for Token<S>

source
impl<S> StructuralEq for Token<S>

source
impl<S> StructuralPartialEq for Token<S>

Auto Trait Implementations

impl<S> RefUnwindSafe for Token<S> where
S: RefUnwindSafe,

impl<S> Send for Token<S> where
S: Send,

impl<S> Sync for Token<S> where
S: Sync,

impl<S> Unpin for Token<S> where
S: Unpin,

impl<S> UnwindSafe for Token<S> where
S: UnwindSafe,

Blanket Implementations

source
impl<T> Any for T where
T: 'static + ?Sized,

source
fn type_id(&self) -> TypeId

~~Gets the TypeId of self. Read more~~

source
impl<T> Borrow<T> for T where
T: ?Sized,

const: unstable · source
fn borrow(&self) -> &T

~~Immutably borrows from an owned value. Read more~~

source
impl<T> BorrowMut<T> for T where
T: ?Sized,

const: unstable · source
fn borrow_mut(&mut self) -> &mut T

~~Mutably borrows from an owned value. Read more~~

source
impl<T> From<T> for T

const: unstable · source
fn from(t: T) -> T

~~Returns the argument unchanged.~~

source
impl<T, U> Into for T where
U: From<T>,

const: unstable · source
fn into(self) -> U

~~Calls U::from(self).~~

~~That is, this conversion is whatever the implementation of From<T> for U chooses to do.~~

source
impl<T> ToString for T where
T: Display + ?Sized,

source
default fn to_string(&self) -> String

~~Converts the given value to a String. Read more~~

source
impl<T, U> TryFrom for T where
U: Into<T>,

~~type Error = Infallible~~

~~The type returned in the event of a conversion error.~~

const: unstable · source
fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

~~Performs the conversion.~~

source
impl<T, U> TryInto for T where
U: TryFrom<T>,

~~type Error = >::Error~~

~~The type returned in the event of a conversion error.~~

const: unstable · source
fn try_into(self) -> Result<U, >::Error>

~~Performs the conversion.~~

Enum dedukti_parse::Token

Variants

Def

Thm

LBrk

RBrk

LPar

RPar

Colon

ColonEq

Arrow

FatArrow

LongArrow

Comma

Dot

Symb(Symb<S>)

Comment(usize)

Error

Trait Implementations

impl<S: Debug> Debug for Token<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

impl<S: Display> Display for Token<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

impl<'s> Logos<'s> for Token<&'s str>

type Extras = ()

type Source = str

fn lex(lex: &mut Lexer<'s, Self>)

fn lexer(source: &'source Self::Source) -> Lexer<'source, Self> where Self::Extras: Default,

fn lexer_with_extras( source: &'source Self::Source, extras: Self::Extras) -> Lexer<'source, Self>

impl<S: PartialEq> PartialEq<Token<S>> for Token<S>

fn eq(&self, other: &Token<S>) -> bool

fn ne(&self, other: &Token<S>) -> bool

impl<S: Eq> Eq for Token<S>

impl<S> StructuralEq for Token<S>

impl<S> StructuralPartialEq for Token<S>

Auto Trait Implementations

impl<S> RefUnwindSafe for Token<S> where S: RefUnwindSafe,

impl<S> Send for Token<S> where S: Send,

impl<S> Sync for Token<S> where S: Sync,

impl<S> Unpin for Token<S> where S: Unpin,

impl<S> UnwindSafe for Token<S> where S: UnwindSafe,

Blanket Implementations

impl<T> Any for T where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

impl<T> Borrow<T> for T where T: ?Sized,

fn borrow(&self) -> &T

impl<T> BorrowMut<T> for T where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

impl<T> From<T> for T

fn from(t: T) -> T

impl<T, U> Into<U> for T where U: From<T>,

fn into(self) -> U

impl<T> ToString for T where T: Display + ?Sized,

default fn to_string(&self) -> String

impl<T, U> TryFrom<U> for T where U: Into<T>,

type Error = Infallible

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

impl<T, U> TryInto<U> for T where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

`Def`

`Thm`

`LBrk`

`RBrk`

`LPar`

`RPar`

`Colon`

`ColonEq`

`Arrow`

`FatArrow`

`LongArrow`

`Comma`

`Dot`

`Symb(Symb<S>)`

`Comment(usize)`

`Error`

fn lexer(source: &'source Self::Source) -> Lexer<'source, Self> where
Self::Extras: Default,

fn lexer_with_extras(
source: &'source Self::Source,
extras: Self::Extras
) -> Lexer<'source, Self>

impl<S> RefUnwindSafe for Token<S> where
S: RefUnwindSafe,

impl<S> Send for Token<S> where
S: Send,

impl<S> Sync for Token<S> where
S: Sync,

impl<S> Unpin for Token<S> where
S: Unpin,

impl<S> UnwindSafe for Token<S> where
S: UnwindSafe,

impl<T> Any for T where
T: 'static + ?Sized,

impl<T> Borrow<T> for T where
T: ?Sized,

impl<T> BorrowMut<T> for T where
T: ?Sized,

impl<T, U> Into<U> for T where
U: From<T>,

impl<T> ToString for T where
T: Display + ?Sized,

impl<T, U> TryFrom<U> for T where
U: Into<T>,

impl<T, U> TryInto<U> for T where
U: TryFrom<T>,