Skip to content

Commit 20ed035

Browse files
committed
implement new parser approach
The new parser has a utility struct, Parser. It supports precedence which lets us cleanup some of the code. The goal is to eventually simplify the Rust types parsing code so we don't need so much scary stuff.
1 parent 6e989ed commit 20ed035

File tree

11 files changed

+1010
-634
lines changed

11 files changed

+1010
-634
lines changed

crates/formality-core/src/cast.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,16 @@ where
216216
}
217217
}
218218

219+
impl<T: Clone, U, E> UpcastFrom<Result<T, E>> for Result<U, E>
220+
where
221+
T: Upcast<U>,
222+
E: Clone,
223+
{
224+
fn upcast_from(term: Result<T, E>) -> Self {
225+
term.map(|t| t.upcast())
226+
}
227+
}
228+
219229
impl DowncastTo<()> for () {
220230
fn downcast_to(&self) -> Option<()> {
221231
Some(())

crates/formality-core/src/language.rs

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,17 @@ pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
2222
+ UpcastFrom<CoreExistentialVar<Self>>
2323
+ UpcastFrom<CoreBoundVar<Self>>;
2424

25-
/// The character (typically `<`) used to open binders.
25+
/// The token (typically `<`) used to open binders.
2626
const BINDING_OPEN: char;
2727

28-
/// The character (typically `>`) used to open binders.
28+
/// The token (typically `>`) used to open binders.
2929
const BINDING_CLOSE: char;
30+
31+
/// Keywords to disallow as identifiers everywhere.
32+
/// It is possible to do positional keywords too, if you want,
33+
/// but it requires custom parsing impls for your types.
34+
/// No fun.
35+
const KEYWORDS: &'static [&'static str];
3036
}
3137

3238
/// For consistency with types like `CoreVariable<L>`, we write `CoreKind<L>` instead of `Kind<L>`.

crates/formality-core/src/lib.rs

Lines changed: 8 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ macro_rules! declare_language {
9090
type Parameter = $param:ty;
9191
const BINDING_OPEN = $binding_open:expr;
9292
const BINDING_CLOSE = $binding_close:expr;
93+
const KEYWORDS = [$($kw:expr),* $(,)?];
9394
}
9495
) => {
9596
$(#[$the_lang_m:meta])*
@@ -105,6 +106,7 @@ macro_rules! declare_language {
105106
type Parameter = $param;
106107
const BINDING_OPEN: char = $binding_open;
107108
const BINDING_CLOSE: char = $binding_close;
109+
const KEYWORDS: &'static [&'static str] = &[$($kw),*];
108110
}
109111

110112
$crate::trait_alias! {
@@ -161,21 +163,7 @@ macro_rules! declare_language {
161163
T: Parse,
162164
B: $crate::Upcast<(String, $param)>,
163165
{
164-
let scope = $crate::parse::Scope::new(bindings.into_iter().map(|b| b.upcast()));
165-
let (t, remainder) = match T::parse(&scope, text) {
166-
Ok(v) => v,
167-
Err(errors) => {
168-
let mut err = $crate::anyhow!("failed to parse {text}");
169-
for error in errors {
170-
err = err.context(error.text.to_owned()).context(error.message);
171-
}
172-
return Err(err);
173-
}
174-
};
175-
if !$crate::parse::skip_whitespace(remainder).is_empty() {
176-
$crate::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}");
177-
}
178-
Ok(t)
166+
$crate::parse::core_term_with::<FormalityLang, T, B>(bindings, text)
179167
}
180168
}
181169
}
@@ -238,12 +226,13 @@ macro_rules! id {
238226

239227
impl CoreParse<crate::FormalityLang> for $n {
240228
fn parse<'t>(
241-
_scope: &parse::Scope<crate::FormalityLang>,
229+
scope: &parse::Scope<crate::FormalityLang>,
242230
text: &'t str,
243231
) -> parse::ParseResult<'t, Self> {
244-
let (string, text) = parse::identifier(text)?;
245-
let n = $n::new(&string);
246-
Ok((n, text))
232+
$crate::parse::Parser::single_variant(scope, text, stringify!($n), |p| {
233+
let string = p.identifier()?;
234+
Ok($n::new(&string))
235+
})
247236
}
248237
}
249238

0 commit comments

Comments
 (0)