Trait formality_core::parse::CoreParse

pub trait CoreParse<L: Language>: Sized + Debug {
    // Required method
    fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>;

    // Provided methods
    fn parse_many<'t>(
        scope: &Scope<L>,
        text: &'t str,
        close_char: char
    ) -> ParseResult<'t, Vec<Self>> { ... }
    fn parse_comma<'t>(
        scope: &Scope<L>,
        text: &'t str,
        close_char: char
    ) -> ParseResult<'t, Vec<Self>> { ... }
}

Trait for parsing a Term<L> as input.

Required Methods

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

Parse a single instance of this type, returning an error if no such instance is present.

Provided Methods

fn parse_many<'t>( scope: &Scope<L>, text: &'t str, close_char: char ) -> ParseResult<'t, Vec<Self>>

Parse many instances of self, expecting close_char to appear after the last instance (close_char is not consumed).

fn parse_comma<'t>( scope: &Scope<L>, text: &'t str, close_char: char ) -> ParseResult<'t, Vec<Self>>

Comma separated list with optional trailing comma.

Object Safety

This trait is not object safe.

Implementations on Foreign Types

impl<L> CoreParse<L> for u32

where L: Language,

fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L> CoreParse<L> for u64

where L: Language,

fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L> CoreParse<L> for usize

where L: Language,

fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L, T> CoreParse<L> for Option<T>

where L: Language, T: CoreParse<L>,

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L, T> CoreParse<L> for Arc<T>

where L: Language, T: CoreParse<L>,

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L, T> CoreParse<L> for Vec<T>

where L: Language, T: CoreParse<L>,

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L: Language> CoreParse<L> for ()

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L: Language, A: CoreParse<L>, B: CoreParse<L>> CoreParse<L> for (A, B)

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

impl<L: Language, A: CoreParse<L>, B: CoreParse<L>, C: CoreParse<L>> CoreParse<L> for (A, B, C)

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

Implementors

impl<L, T> CoreParse<L> for CoreBinder<L, T>

where L: Language, T: CoreTerm<L>,

Parse a binder: find the names in scope, parse the contents, and then replace names with debruijn indices.

impl<L, T> CoreParse<L> for Set<T>

where L: Language, T: CoreParse<L> + Ord,

impl<L: Language> CoreParse<L> for Binding<L>

Binding grammar is $kind $name, e.g., ty Foo.