Skip to content

Commit 651b3c4

Browse files
joshlfjoshlf
committed
[WIP]
gherrit-pr-id: Ib659c95874d275713cc813788024b49e87a8873d
1 parent c123e30 commit 651b3c4

File tree

1 file changed

+72
-51
lines changed

1 file changed

+72
-51
lines changed

‎tools/hermes/src/parse.rs‎

Lines changed: 72 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
use std::{
2+
convert::Infallible,
23
fs, io,
34
ops::Range,
45
path::{Path, PathBuf},
@@ -84,17 +85,17 @@ impl TypeItem {
8485
}
8586

8687
#[derive(Clone, Debug)]
87-
pub struct HermesDecorated<T, A = std::convert::Infallible> {
88+
pub struct HermesDecorated<T, A = Infallible> {
8889
pub item: T,
8990
pub hermes: attr::HermesBlock<A>,
9091
}
9192

9293
#[derive(Clone, Debug)]
9394
pub enum ParsedItem {
9495
Function(HermesDecorated<FunctionItem, attr::HermesAttr>),
95-
Type(HermesDecorated<TypeItem, std::convert::Infallible>),
96-
Trait(HermesDecorated<ItemTrait, std::convert::Infallible>),
97-
Impl(HermesDecorated<ItemImpl, std::convert::Infallible>),
96+
Type(HermesDecorated<TypeItem, Infallible>),
97+
Trait(HermesDecorated<ItemTrait, Infallible>),
98+
Impl(HermesDecorated<ItemImpl, Infallible>),
9899
}
99100

100101
impl ParsedItem {
@@ -118,41 +119,41 @@ impl ParsedItem {
118119
}
119120
}
120121

121-
fn convert_block_infallible(
122+
/// Convert from a pair of `item` and `block: HermesBlock<HermesAttr>` to a
123+
/// `HermesDecorated<Infallible>`, erroring if the `block` has an attribute.
124+
///
125+
/// On success, pass the `HermesDecorate<Infallible>` to `f`.
126+
fn try_from_raw_reject_attr<T, F: FnOnce(HermesDecorated<T>) -> ParsedItem>(
127+
item: T,
122128
block: attr::HermesBlock<attr::HermesAttr>,
123-
) -> Result<attr::HermesBlock<std::convert::Infallible>, HermesError> {
129+
f: F,
130+
) -> Result<ParsedItem, HermesError> {
124131
if let Some(_attr) = block.attribute {
125132
return Err(HermesError::DocBlockError {
126-
src: NamedSource::new("TODO", "TODO".to_string()), // We fix this up in process_item
133+
// TODO
134+
src: NamedSource::new("TODO", "TODO".to_string()),
127135
span: span_to_miette(block.start_span),
128136
msg: "This item does not support Hermes attributes (like `spec` or `unsafe(axiom)`). Only generic `hermes` blocks are allowed.".to_string(),
129137
});
130138
}
131-
Ok(attr::HermesBlock {
132-
attribute: None,
133-
content: block.content,
134-
content_span: block.content_span,
135-
start_span: block.start_span,
136-
})
139+
Ok(f(HermesDecorated {
140+
item,
141+
hermes: attr::HermesBlock {
142+
attribute: None,
143+
content: block.content,
144+
content_span: block.content_span,
145+
start_span: block.start_span,
146+
},
147+
}))
137148
}
138149

139-
fn try_from_raw_reject_attr<T, F: FnOnce(HermesDecorated<T>) -> ParsedItem>(
140-
item: T,
141-
block: attr::HermesBlock<attr::HermesAttr>,
142-
f: F,
143-
) -> Result<ParsedItem, HermesError> {
144-
let hermes = convert_block_infallible(block)?;
145-
Ok(f(HermesDecorated { item, hermes }))
146-
}
150+
// TODO: Merge this with `HermesDecorated`?
147151

148-
/// A complete parsed item including its module path and the extracted Lean block.
152+
/// A complete parsed item including its module path and source file.
149153
#[derive(Debug)]
150154
pub struct ParsedLeanItem {
151155
pub item: ParsedItem,
152156
pub module_path: Vec<String>,
153-
#[allow(dead_code)] // TODO: Remove if truly unused
154-
lean_block: String,
155-
#[allow(dead_code)]
156157
source_file: Option<PathBuf>,
157158
}
158159

@@ -273,7 +274,6 @@ where
273274
I: FnMut(&str, Result<ParsedLeanItem, HermesError>),
274275
M: FnMut(UnloadedModule),
275276
{
276-
//fn try_from_raw_reject_attr<T, F: FnOnce(T) -> ParsedItem + Default>(item: T, attr: Option<attr::HermesAttr>) -> Result<ParsedItem, HermesError> {
277277
fn process_item<
278278
T,
279279
F: FnOnce(T, attr::HermesBlock<attr::HermesAttr>) -> Result<ParsedItem, HermesError>,
@@ -286,9 +286,10 @@ where
286286
) {
287287
let block = match attr::extract_hermes_block(attrs) {
288288
Ok(Some(b)) => b,
289-
Ok(None) => return, // No Hermes block, skip
289+
// This item doesn't have a Hermes annotation; skip it.
290+
Ok(None) => return,
290291
Err(e) => {
291-
debug!("Error extracting ```lean block: {}", e);
292+
log::trace!("Error extracting ```lean block: {}", e);
292293
(self.item_cb)(
293294
&self.source_code.as_str()[span.byte_range()],
294295
Err(HermesError::DocBlockError {
@@ -302,26 +303,27 @@ where
302303
};
303304

304305
if self.inside_block {
305-
(self.item_cb)(
306+
(self.item_cb)(
306307
&self.source_code.as_str()[span.byte_range()],
307308
Err(HermesError::NestedItemError {
308309
src: self.named_source.clone(),
309310
span: span_to_miette(span),
310-
msg: "Hermes cannot verify items defined inside function bodies or other blocks.".to_string(),
311+
msg:
312+
"Hermes cannot verify items defined inside function bodies or other blocks."
313+
.to_string(),
311314
}),
312315
);
313316
return;
314317
}
315318

316-
let Range { start, end } = span.byte_range();
317-
let source = &self.source_code.as_str()[start..end];
319+
let source = &self.source_code.as_str()[span.byte_range()];
318320

319-
// Clone fields needed for ParsedLeanItem construction before moving block
320-
let lean_block_content = block.content.clone();
321-
322321
let parsed_item = match f(item, block) {
323322
Ok(i) => i,
324323
Err(mut e) => {
324+
// TODO: What is the point of this? Why are we special-casing
325+
// `TODO`?
326+
325327
// If it's a DocBlockError that needs source context, ensure we provide it
326328
if let HermesError::DocBlockError { src, .. } = &mut e {
327329
if src.name() == "TODO" {
@@ -338,7 +340,6 @@ where
338340
Ok(ParsedLeanItem {
339341
item: parsed_item,
340342
module_path: self.current_path.clone(),
341-
lean_block: lean_block_content,
342343
source_file: self.source_file.clone(),
343344
}),
344345
);
@@ -353,7 +354,7 @@ where
353354
fn visit_item_mod(&mut self, node: &'ast ItemMod) {
354355
let mod_name = node.ident.to_string();
355356

356-
// Check for unloaded modules (mod foo;)
357+
// Unloaded module (i.e., `mod foo;`).
357358
if node.content.is_none() {
358359
(self.mod_cb)(UnloadedModule {
359360
name: mod_name.clone(),
@@ -383,31 +384,46 @@ where
383384
fn visit_item_fn(&mut self, node: &'ast ItemFn) {
384385
trace!("Visiting Fn {}", node.sig.ident);
385386
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
386-
Ok(ParsedItem::Function(HermesDecorated { item: FunctionItem::Free(item), hermes: block }))
387+
Ok(ParsedItem::Function(HermesDecorated {
388+
item: FunctionItem::Free(item),
389+
hermes: block,
390+
}))
387391
});
388392
syn::visit::visit_item_fn(self, node);
389393
}
390394

391395
fn visit_item_struct(&mut self, node: &'ast ItemStruct) {
392396
trace!("Visiting Struct {}", node.ident);
393397
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
394-
try_from_raw_reject_attr(item, block, |d| ParsedItem::Type(HermesDecorated { item: TypeItem::Struct(d.item), hermes: d.hermes }))
398+
try_from_raw_reject_attr(item, block, |d| {
399+
ParsedItem::Type(HermesDecorated {
400+
item: TypeItem::Struct(d.item),
401+
hermes: d.hermes,
402+
})
403+
})
395404
});
396405
syn::visit::visit_item_struct(self, node);
397406
}
398407

399408
fn visit_item_enum(&mut self, node: &'ast ItemEnum) {
400409
trace!("Visiting Enum {}", node.ident);
401410
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
402-
try_from_raw_reject_attr(item, block, |d| ParsedItem::Type(HermesDecorated { item: TypeItem::Enum(d.item), hermes: d.hermes }))
411+
try_from_raw_reject_attr(item, block, |d| {
412+
ParsedItem::Type(HermesDecorated { item: TypeItem::Enum(d.item), hermes: d.hermes })
413+
})
403414
});
404415
syn::visit::visit_item_enum(self, node);
405416
}
406417

407418
fn visit_item_union(&mut self, node: &'ast ItemUnion) {
408419
trace!("Visiting Union {}", node.ident);
409420
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
410-
try_from_raw_reject_attr(item, block, |d| ParsedItem::Type(HermesDecorated { item: TypeItem::Union(d.item), hermes: d.hermes }))
421+
try_from_raw_reject_attr(item, block, |d| {
422+
ParsedItem::Type(HermesDecorated {
423+
item: TypeItem::Union(d.item),
424+
hermes: d.hermes,
425+
})
426+
})
411427
});
412428
syn::visit::visit_item_union(self, node);
413429
}
@@ -442,15 +458,21 @@ where
442458
fn visit_impl_item_fn(&mut self, node: &'ast ImplItemFn) {
443459
trace!("Visiting ImplItemFn {}", node.sig.ident);
444460
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
445-
Ok(ParsedItem::Function(HermesDecorated { item: FunctionItem::Impl(item), hermes: block }))
461+
Ok(ParsedItem::Function(HermesDecorated {
462+
item: FunctionItem::Impl(item),
463+
hermes: block,
464+
}))
446465
});
447466
syn::visit::visit_impl_item_fn(self, node);
448467
}
449468

450469
fn visit_trait_item_fn(&mut self, node: &'ast TraitItemFn) {
451470
trace!("Visiting TraitItemFn {}", node.sig.ident);
452471
self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| {
453-
Ok(ParsedItem::Function(HermesDecorated { item: FunctionItem::Trait(item), hermes: block }))
472+
Ok(ParsedItem::Function(HermesDecorated {
473+
item: FunctionItem::Trait(item),
474+
hermes: block,
475+
}))
454476
});
455477
syn::visit::visit_trait_item_fn(self, node);
456478
}
@@ -460,7 +482,6 @@ where
460482
/// Returns `Ok(None)` if no block is found.
461483
/// Returns `Err` if the block is malformed or multiple blocks are found.
462484
463-
464485
/// Extracts the `...` from the first `#[path = "..."]` attribute found, if any.
465486
fn extract_path_attr(attrs: &[Attribute]) -> Option<String> {
466487
for attr in attrs {
@@ -511,8 +532,6 @@ fn span_to_miette(span: proc_macro2::Span) -> SourceSpan {
511532
}
512533

513534
mod attr {
514-
use std::convert::Infallible;
515-
516535
use proc_macro2::Span;
517536

518537
use super::*;
@@ -600,7 +619,9 @@ mod attr {
600619
}
601620

602621
/// Helper to parse and extract a single Hermes block from a slice of attributes.
603-
pub fn extract_hermes_block(attrs: &[Attribute]) -> Result<Option<HermesBlock<HermesAttr>>, Error> {
622+
pub fn extract_hermes_block(
623+
attrs: &[Attribute],
624+
) -> Result<Option<HermesBlock<HermesAttr>>, Error> {
604625
let mut found_block: Option<HermesBlock<HermesAttr>> = None;
605626
let mut iter = attrs.iter().peekable();
606627

@@ -812,17 +833,17 @@ mod tests {
812833
"#;
813834
let items = parse_to_vec(code);
814835
assert_eq!(items.len(), 2);
815-
836+
816837
let (src1, item1) = &items[0];
817838
let (src2, item2) = &items[1];
818-
839+
819840
let i1 = item1.as_ref().unwrap();
820841
let i2 = item2.as_ref().unwrap();
821-
842+
822843
// Verify we got the right blocks for the right items
823844
assert!(i1.lean_block.contains("theorem a"));
824845
assert!(i2.lean_block.contains("theorem b"));
825-
846+
826847
// Verify source snippets match the function definition + doc comment
827848
assert!(src1.contains("theorem a"));
828849
assert!(src1.contains("fn foo"));

0 commit comments

Comments
 (0)