Skip to content

Commit d92de78

Browse files
committed
[hermes] Add source code transformation
gherrit-pr-id: G9611b9a3ca0254d8ba488d591e6a21980cca3d29
1 parent cdbf265 commit d92de78

File tree

4 files changed

+229
-61
lines changed

4 files changed

+229
-61
lines changed

tools/hermes/src/main.rs

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
mod errors;
22
mod parse;
3+
mod transform;
34
mod ui_test_shim;
45

5-
use std::{env, fs, path::PathBuf, process::exit};
6+
use std::{env, path::PathBuf, process::exit};
67

78
fn main() {
89
if env::var("HERMES_UI_TEST_MODE").is_ok() {
@@ -17,23 +18,27 @@ fn main() {
1718
}
1819

1920
let file_path = PathBuf::from(&args[1]);
20-
let source = match fs::read_to_string(&file_path) {
21-
Ok(s) => s,
22-
Err(e) => {
23-
eprintln!("Error reading file: {}", e);
24-
exit(1);
25-
}
26-
};
2721

2822
let mut has_errors = false;
29-
parse::visit_hermes_items_in_file(&file_path, &source, |res| {
23+
let mut edits = Vec::new();
24+
let res = parse::read_file_and_visit_hermes_items(&file_path, |_src, res| {
3025
if let Err(e) = res {
3126
has_errors = true;
3227
eprint!("{:?}", miette::Report::new(e));
28+
} else if let Ok(item) = res {
29+
transform::append_edits(&item, &mut edits);
3330
}
3431
});
3532

33+
let source = res.unwrap_or_else(|e| {
34+
eprintln!("Error parsing file: {}", e);
35+
exit(1);
36+
});
37+
3638
if has_errors {
3739
exit(1);
3840
}
41+
42+
let mut source = source.into_bytes();
43+
transform::apply_edits(&mut source, &edits);
3944
}

tools/hermes/src/parse.rs

Lines changed: 111 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,15 @@
1-
use std::path::{Path, PathBuf};
1+
use std::{
2+
fs, io,
3+
ops::Range,
4+
path::{Path, PathBuf},
5+
};
26

37
use log::{debug, trace};
48
use miette::{NamedSource, SourceSpan};
9+
use proc_macro2::Span;
510
use syn::{
6-
visit::Visit, Attribute, Error, Expr, ItemEnum, ItemFn, ItemImpl, ItemMod, ItemStruct,
7-
ItemTrait, ItemUnion, Lit, Meta,
11+
spanned::Spanned as _, visit::Visit, Attribute, Error, Expr, ItemEnum, ItemFn, ItemImpl,
12+
ItemMod, ItemStruct, ItemTrait, ItemUnion, Lit, Meta,
813
};
914

1015
use crate::errors::HermesError;
@@ -30,7 +35,7 @@ impl std::error::Error for ParseError {}
3035

3136
/// The item from the original source code.
3237
#[derive(Clone, Debug)]
33-
enum ParsedItem {
38+
pub enum ParsedItem {
3439
Fn(ItemFn),
3540
Struct(ItemStruct),
3641
Enum(ItemEnum),
@@ -56,7 +61,7 @@ impl ParsedItem {
5661
/// A complete parsed item including its module path and the extracted Lean block.
5762
#[derive(Debug)]
5863
pub struct ParsedLeanItem {
59-
item: ParsedItem,
64+
pub item: ParsedItem,
6065
module_path: Vec<String>,
6166
lean_block: String,
6267
source_file: Option<PathBuf>,
@@ -67,26 +72,28 @@ pub struct ParsedLeanItem {
6772
///
6873
/// If parsing fails, or if any item has multiple Lean blocks, the callback is
6974
/// invoked with an `Err`.
70-
fn visit_hermes_items<F>(source: &str, f: F)
75+
pub fn visit_hermes_items<F>(source: &str, f: F)
7176
where
72-
F: FnMut(Result<ParsedLeanItem, HermesError>),
77+
F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
7378
{
7479
visit_hermes_items_internal(source, None, f)
7580
}
7681

7782
/// Parses the given Rust source code from a file path and invokes the callback `f`
7883
/// for each item annotated with a `/// ```lean` block. Parsing errors and generated
7984
/// items will be associated with this file path.
80-
pub fn visit_hermes_items_in_file<F>(path: &Path, source: &str, f: F)
85+
pub fn read_file_and_visit_hermes_items<F>(path: &Path, f: F) -> Result<String, io::Error>
8186
where
82-
F: FnMut(Result<ParsedLeanItem, HermesError>),
87+
F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
8388
{
84-
visit_hermes_items_internal(source, Some(path.to_path_buf()), f)
89+
let source = fs::read_to_string(path).expect("Failed to read file");
90+
visit_hermes_items_internal(&source, Some(path.to_path_buf()), f);
91+
Ok(source)
8592
}
8693

8794
fn visit_hermes_items_internal<F>(source: &str, source_file: Option<PathBuf>, mut f: F)
8895
where
89-
F: FnMut(Result<ParsedLeanItem, HermesError>),
96+
F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
9097
{
9198
trace!("Parsing source code into syn::File");
9299
let file_name = {
@@ -109,11 +116,14 @@ where
109116
}
110117
Err(e) => {
111118
debug!("Failed to parse source code: {}", e);
112-
f(Err(HermesError::SynError {
113-
src: named_source.clone(),
114-
span: span_to_miette(e.span()),
115-
msg: e.to_string(),
116-
}));
119+
f(
120+
source,
121+
Err(HermesError::SynError {
122+
src: named_source.clone(),
123+
span: span_to_miette(e.span()),
124+
msg: e.to_string(),
125+
}),
126+
);
117127
return;
118128
}
119129
};
@@ -141,39 +151,48 @@ struct HermesVisitor<F> {
141151

142152
impl<F> HermesVisitor<F>
143153
where
144-
F: FnMut(Result<ParsedLeanItem, HermesError>),
154+
F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
145155
{
146-
fn check_and_add(&mut self, item: ParsedItem) {
156+
fn check_and_add(&mut self, item: ParsedItem, span: Span) {
157+
let Range { start, end } = span.byte_range();
158+
let source = &self.source_code.as_str()[start..end];
159+
147160
let attrs = item.attrs();
148161
trace!("Checking item in module path `{:?}` for ```lean block", self.current_path);
149162
match extract_lean_block(attrs) {
150163
Ok(Some(lean_block)) => {
151164
debug!("Found valid ```lean block for item in `{:?}`", self.current_path);
152-
(self.callback)(Ok(ParsedLeanItem {
153-
item,
154-
module_path: self.current_path.clone(),
155-
lean_block,
156-
source_file: self.source_file.clone(),
157-
}));
165+
(self.callback)(
166+
source,
167+
Ok(ParsedLeanItem {
168+
item,
169+
module_path: self.current_path.clone(),
170+
lean_block,
171+
source_file: self.source_file.clone(),
172+
}),
173+
);
158174
}
159175
Ok(None) => {
160176
trace!("No ```lean block found for item");
161177
} // Skip item
162178
Err(e) => {
163179
debug!("Error extracting ```lean block: {}", e);
164-
(self.callback)(Err(HermesError::DocBlockError {
165-
src: self.named_source.clone(),
166-
span: span_to_miette(e.span()),
167-
msg: e.to_string(),
168-
}));
180+
(self.callback)(
181+
source,
182+
Err(HermesError::DocBlockError {
183+
src: self.named_source.clone(),
184+
span: span_to_miette(e.span()),
185+
msg: e.to_string(),
186+
}),
187+
);
169188
}
170189
}
171190
}
172191
}
173192

174193
impl<'ast, F> Visit<'ast> for HermesVisitor<F>
175194
where
176-
F: FnMut(Result<ParsedLeanItem, HermesError>),
195+
F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
177196
{
178197
fn visit_item_mod(&mut self, node: &'ast ItemMod) {
179198
let mod_name = node.ident.to_string();
@@ -186,37 +205,37 @@ where
186205

187206
fn visit_item_fn(&mut self, node: &'ast ItemFn) {
188207
trace!("Visiting Fn {}", node.sig.ident);
189-
self.check_and_add(ParsedItem::Fn(node.clone()));
208+
self.check_and_add(ParsedItem::Fn(node.clone()), node.span());
190209
syn::visit::visit_item_fn(self, node);
191210
}
192211

193212
fn visit_item_struct(&mut self, node: &'ast ItemStruct) {
194213
trace!("Visiting Struct {}", node.ident);
195-
self.check_and_add(ParsedItem::Struct(node.clone()));
214+
self.check_and_add(ParsedItem::Struct(node.clone()), node.span());
196215
syn::visit::visit_item_struct(self, node);
197216
}
198217

199218
fn visit_item_enum(&mut self, node: &'ast ItemEnum) {
200219
trace!("Visiting Enum {}", node.ident);
201-
self.check_and_add(ParsedItem::Enum(node.clone()));
220+
self.check_and_add(ParsedItem::Enum(node.clone()), node.span());
202221
syn::visit::visit_item_enum(self, node);
203222
}
204223

205224
fn visit_item_union(&mut self, node: &'ast ItemUnion) {
206225
trace!("Visiting Union {}", node.ident);
207-
self.check_and_add(ParsedItem::Union(node.clone()));
226+
self.check_and_add(ParsedItem::Union(node.clone()), node.span());
208227
syn::visit::visit_item_union(self, node);
209228
}
210229

211230
fn visit_item_trait(&mut self, node: &'ast ItemTrait) {
212231
trace!("Visiting Trait {}", node.ident);
213-
self.check_and_add(ParsedItem::Trait(node.clone()));
232+
self.check_and_add(ParsedItem::Trait(node.clone()), node.span());
214233
syn::visit::visit_item_trait(self, node);
215234
}
216235

217236
fn visit_item_impl(&mut self, node: &'ast ItemImpl) {
218237
trace!("Visiting Impl");
219-
self.check_and_add(ParsedItem::Impl(node.clone()));
238+
self.check_and_add(ParsedItem::Impl(node.clone()), node.span());
220239
syn::visit::visit_item_impl(self, node);
221240
}
222241
}
@@ -319,9 +338,9 @@ mod tests {
319338

320339
use super::*;
321340

322-
fn parse_to_vec(code: &str) -> Vec<Result<ParsedLeanItem, HermesError>> {
341+
fn parse_to_vec(code: &str) -> Vec<(String, Result<ParsedLeanItem, HermesError>)> {
323342
let mut items = Vec::new();
324-
visit_hermes_items(code, |res| items.push(res));
343+
visit_hermes_items(code, |src, res| items.push((src.to_string(), res)));
325344
items
326345
}
327346

@@ -334,7 +353,15 @@ mod tests {
334353
fn foo() {}
335354
"#;
336355
let items = parse_to_vec(code);
337-
let item = items.into_iter().next().unwrap().unwrap();
356+
let (src, res) = items.into_iter().next().unwrap();
357+
let item = res.unwrap();
358+
assert_eq!(
359+
src,
360+
"/// ```lean
361+
/// theorem foo : True := by trivial
362+
/// ```
363+
fn foo() {}"
364+
);
338365
assert!(matches!(item.item, ParsedItem::Fn(_)));
339366
assert_eq!(item.lean_block, " ```lean\n theorem foo : True := by trivial\n ```\n");
340367
assert!(item.source_file.is_none());
@@ -352,7 +379,18 @@ mod tests {
352379
fn foo() {}
353380
"#;
354381
let items = parse_to_vec(code);
355-
let err = items.into_iter().next().unwrap().unwrap_err();
382+
let (src, res) = items.into_iter().next().unwrap();
383+
let err = res.unwrap_err();
384+
assert_eq!(
385+
src,
386+
"/// ```lean
387+
/// a
388+
/// ```
389+
/// ```lean
390+
/// b
391+
/// ```
392+
fn foo() {}"
393+
);
356394
assert!(err.to_string().contains("Multiple lean blocks"));
357395
}
358396

@@ -364,7 +402,14 @@ mod tests {
364402
fn foo() {}
365403
"#;
366404
let items = parse_to_vec(code);
367-
let err = items.into_iter().next().unwrap().unwrap_err();
405+
let (src, res) = items.into_iter().next().unwrap();
406+
let err = res.unwrap_err();
407+
assert_eq!(
408+
src,
409+
"/// ```lean
410+
/// a
411+
fn foo() {}"
412+
);
368413
assert!(err.to_string().contains("Unclosed"));
369414
}
370415

@@ -380,7 +425,14 @@ mod tests {
380425
}
381426
"#;
382427
let items = parse_to_vec(code);
383-
let item = items.into_iter().next().unwrap().unwrap();
428+
let (src, res) = items.into_iter().next().unwrap();
429+
let item = res.unwrap();
430+
assert_eq!(
431+
src,
432+
"/// ```lean
433+
/// ```
434+
fn foo() {}"
435+
);
384436
assert_eq!(item.module_path, vec!["a", "b"]);
385437
}
386438

@@ -392,9 +444,20 @@ mod tests {
392444
fn foo() {}
393445
"#;
394446
let mut items = Vec::new();
395-
visit_hermes_items_in_file(Path::new("src/foo.rs"), code, |res| items.push(res));
396-
let err = items.into_iter().next().unwrap().unwrap_err();
397-
let rep = format!("{:?}", miette::Report::new(err));
447+
visit_hermes_items_internal(
448+
code,
449+
Some(Path::new("src/foo.rs").to_path_buf()),
450+
|source: &str, res| items.push((source.to_string(), res)),
451+
);
452+
let (src, res) = items.into_iter().next().unwrap();
453+
assert_eq!(
454+
src,
455+
"/// ```lean
456+
/// a
457+
fn foo() {}"
458+
);
459+
460+
let rep = format!("{:?}", miette::Report::new(res.unwrap_err()));
398461
assert!(rep.contains("src/foo.rs"));
399462
assert!(rep.contains("Unclosed"));
400463
}
@@ -417,7 +480,7 @@ mod c {
417480
}
418481
";
419482
let mut items = Vec::new();
420-
visit_hermes_items(source, |res| items.push(res));
483+
visit_hermes_items(source, |_src, res| items.push(res));
421484
let i1 = items[0].as_ref().unwrap();
422485
let i2 = items[1].as_ref().unwrap();
423486

@@ -464,8 +527,8 @@ mod c {
464527
let path = std::path::Path::new("src/foo.rs");
465528
let mut items = Vec::new();
466529

467-
visit_hermes_items_in_file(path, code1, |res| items.push(res));
468-
visit_hermes_items_in_file(path, code2, |res| items.push(res));
530+
visit_hermes_items_internal(code1, Some(path.to_path_buf()), |_src, res| items.push(res));
531+
visit_hermes_items_internal(code2, Some(path.to_path_buf()), |_src, res| items.push(res));
469532

470533
let mut report_string = String::new();
471534
for err in items.into_iter().filter_map(|r| r.err()) {

0 commit comments

Comments
 (0)