1- use std:: path:: { Path , PathBuf } ;
1+ use std:: {
2+ fs, io,
3+ ops:: Range ,
4+ path:: { Path , PathBuf } ,
5+ } ;
26
37use log:: { debug, trace} ;
48use miette:: { NamedSource , SourceSpan } ;
9+ use proc_macro2:: Span ;
510use 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
1015use 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 ) ]
5863pub 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 )
7176where
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 >
8186where
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
8794fn visit_hermes_items_internal < F > ( source : & str , source_file : Option < PathBuf > , mut f : F )
8895where
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
142152impl < F > HermesVisitor < F >
143153where
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
174193impl < ' ast , F > Visit < ' ast > for HermesVisitor < F >
175194where
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