@@ -6,7 +6,7 @@ use crate::{
66 Expression , Function , Line , Program , Scope , SimpleExpr , Var ,
77 } ,
88} ;
9- use lean_vm:: { Boolean , BooleanExpr , SourceLineNumber , Table , TableT } ;
9+ use lean_vm:: { Boolean , BooleanExpr , FileId , SourceLineNumber , SourceLocation , Table , TableT } ;
1010use std:: {
1111 collections:: { BTreeMap , BTreeSet } ,
1212 fmt:: { Display , Formatter } ,
@@ -21,6 +21,7 @@ pub struct SimpleProgram {
2121#[ derive( Debug , Clone ) ]
2222pub struct SimpleFunction {
2323 pub name : String ,
24+ pub file_id : FileId ,
2425 pub arguments : Vec < Var > ,
2526 pub n_returned_vars : usize ,
2627 pub instructions : Vec < SimpleLine > ,
@@ -146,7 +147,7 @@ pub enum SimpleLine {
146147 } ,
147148 // noop, debug purpose only
148149 LocationReport {
149- location : SourceLineNumber ,
150+ location : SourceLocation ,
150151 } ,
151152 DebugAssert ( BooleanExpr < SimpleExpr > , SourceLineNumber ) ,
152153}
@@ -190,6 +191,7 @@ pub fn simplify_program(mut program: Program) -> SimpleProgram {
190191 let mut array_manager = ArrayManager :: default ( ) ;
191192 let simplified_instructions = simplify_lines (
192193 & program. functions ,
194+ func. file_id ,
193195 func. n_returned_vars ,
194196 & func. body ,
195197 & mut counters,
@@ -209,6 +211,7 @@ pub fn simplify_program(mut program: Program) -> SimpleProgram {
209211 . collect :: < Vec < _ > > ( ) ;
210212 let simplified_function = SimpleFunction {
211213 name : name. clone ( ) ,
214+ file_id : func. file_id ,
212215 arguments,
213216 n_returned_vars : func. n_returned_vars ,
214217 instructions : simplified_instructions,
@@ -600,6 +603,7 @@ impl ArrayManager {
600603#[ allow( clippy:: too_many_arguments) ]
601604fn simplify_lines (
602605 functions : & BTreeMap < String , Function > ,
606+ file_id : FileId ,
603607 n_returned_vars : usize ,
604608 lines : & [ Line ] ,
605609 counters : & mut Counters ,
@@ -622,6 +626,7 @@ fn simplify_lines(
622626 assert_eq ! ( * pattern, i, "match patterns should be consecutive, starting from 0" ) ;
623627 simple_arms. push ( simplify_lines (
624628 functions,
629+ file_id,
625630 n_returned_vars,
626631 statements,
627632 counters,
@@ -812,6 +817,7 @@ fn simplify_lines(
812817 let mut array_manager_then = array_manager. clone ( ) ;
813818 let then_branch_simplified = simplify_lines (
814819 functions,
820+ file_id,
815821 n_returned_vars,
816822 then_branch,
817823 counters,
@@ -826,6 +832,7 @@ fn simplify_lines(
826832
827833 let else_branch_simplified = simplify_lines (
828834 functions,
835+ file_id,
829836 n_returned_vars,
830837 else_branch,
831838 counters,
@@ -874,6 +881,7 @@ fn simplify_lines(
874881 array_manager. valid . clear ( ) ;
875882 let simplified_body = simplify_lines (
876883 functions,
884+ file_id,
877885 0 ,
878886 body,
879887 counters,
@@ -938,7 +946,10 @@ fn simplify_lines(
938946 // Create recursive function body
939947 let recursive_func = create_recursive_function (
940948 func_name. clone ( ) ,
941- * line_number,
949+ SourceLocation {
950+ line_number : * line_number,
951+ file_id,
952+ } ,
942953 func_args,
943954 iterator. clone ( ) ,
944955 end_simplified,
@@ -1122,7 +1133,12 @@ fn simplify_lines(
11221133 res. push ( SimpleLine :: Panic ) ;
11231134 }
11241135 Line :: LocationReport { location } => {
1125- res. push ( SimpleLine :: LocationReport { location : * location } ) ;
1136+ res. push ( SimpleLine :: LocationReport {
1137+ location : SourceLocation {
1138+ line_number : * location,
1139+ file_id,
1140+ } ,
1141+ } ) ;
11261142 }
11271143 }
11281144 }
@@ -1161,10 +1177,7 @@ fn simplify_expr(
11611177 ) ;
11621178 }
11631179 }
1164- panic ! (
1165- "Const array '{}' can only be accessed with compile-time constant indices" ,
1166- array_var
1167- ) ;
1180+ panic ! ( "Const array '{array_var}' can only be accessed with compile-time constant indices" , ) ;
11681181 }
11691182
11701183 if let SimpleExpr :: Var ( array_var) = array
@@ -1672,7 +1685,7 @@ fn handle_array_assignment(
16721685
16731686fn create_recursive_function (
16741687 name : String ,
1675- line_number : SourceLineNumber ,
1688+ location : SourceLocation ,
16761689 args : Vec < Var > ,
16771690 iterator : Var ,
16781691 end : SimpleExpr ,
@@ -1696,7 +1709,7 @@ fn create_recursive_function(
16961709 function_name : name. clone ( ) ,
16971710 args : recursive_args,
16981711 return_data : vec ! [ ] ,
1699- line_number,
1712+ line_number : location . line_number ,
17001713 } ) ;
17011714 body. push ( SimpleLine :: FunctionRet { return_data : vec ! [ ] } ) ;
17021715
@@ -1713,12 +1726,13 @@ fn create_recursive_function(
17131726 condition: diff_var. into( ) ,
17141727 then_branch: body,
17151728 else_branch: vec![ SimpleLine :: FunctionRet { return_data: vec![ ] } ] ,
1716- line_number,
1729+ line_number: location . line_number ,
17171730 } ,
17181731 ] ;
17191732
17201733 SimpleFunction {
17211734 name,
1735+ file_id : location. file_id ,
17221736 arguments : args,
17231737 n_returned_vars : 0 ,
17241738 instructions,
@@ -2109,6 +2123,7 @@ fn handle_const_arguments(program: &mut Program) -> bool {
21092123 for func in program. functions . values_mut ( ) {
21102124 if !func. has_const_arguments ( ) {
21112125 any_changes |= handle_const_arguments_helper (
2126+ func. file_id ,
21122127 & mut func. body ,
21132128 & constant_functions,
21142129 & mut new_functions,
@@ -2133,6 +2148,7 @@ fn handle_const_arguments(program: &mut Program) -> bool {
21332148 if let Some ( func) = new_functions. get_mut ( & name) {
21342149 let initial_count = additional_functions. len ( ) ;
21352150 handle_const_arguments_helper (
2151+ func. file_id ,
21362152 & mut func. body ,
21372153 & constant_functions,
21382154 & mut additional_functions,
@@ -2169,6 +2185,7 @@ fn handle_const_arguments(program: &mut Program) -> bool {
21692185}
21702186
21712187fn handle_const_arguments_helper (
2188+ file_id : FileId ,
21722189 lines : & mut [ Line ] ,
21732190 constant_functions : & BTreeMap < String , Function > ,
21742191 new_functions : & mut BTreeMap < String , Function > ,
@@ -2228,6 +2245,7 @@ fn handle_const_arguments_helper(
22282245 const_funct_name. clone ( ) ,
22292246 Function {
22302247 name : const_funct_name,
2248+ file_id,
22312249 arguments : func
22322250 . arguments
22332251 . iter ( )
@@ -2247,15 +2265,29 @@ fn handle_const_arguments_helper(
22472265 else_branch,
22482266 ..
22492267 } => {
2250- changed |= handle_const_arguments_helper ( then_branch, constant_functions, new_functions, const_arrays) ;
2251- changed |= handle_const_arguments_helper ( else_branch, constant_functions, new_functions, const_arrays) ;
2268+ changed |= handle_const_arguments_helper (
2269+ file_id,
2270+ then_branch,
2271+ constant_functions,
2272+ new_functions,
2273+ const_arrays,
2274+ ) ;
2275+ changed |= handle_const_arguments_helper (
2276+ file_id,
2277+ else_branch,
2278+ constant_functions,
2279+ new_functions,
2280+ const_arrays,
2281+ ) ;
22522282 }
22532283 Line :: ForLoop { body, unroll : _, .. } => {
2254- changed |= handle_const_arguments_helper ( body, constant_functions, new_functions, const_arrays) ;
2284+ // TODO we should unroll before const arguments handling
2285+ handle_const_arguments_helper ( file_id, body, constant_functions, new_functions, const_arrays) ;
22552286 }
22562287 Line :: Match { arms, .. } => {
22572288 for ( _, arm) in arms {
2258- changed |= handle_const_arguments_helper ( arm, constant_functions, new_functions, const_arrays) ;
2289+ changed |=
2290+ handle_const_arguments_helper ( file_id, arm, constant_functions, new_functions, const_arrays) ;
22592291 }
22602292 }
22612293 _ => { }
@@ -2565,7 +2597,7 @@ impl SimpleLine {
25652597 Self :: Panic => "panic" . to_string ( ) ,
25662598 Self :: LocationReport { .. } => Default :: default ( ) ,
25672599 Self :: DebugAssert ( bool, _) => {
2568- format ! ( "debug_assert({})" , bool )
2600+ format ! ( "debug_assert({bool })" )
25692601 }
25702602 } ;
25712603 format ! ( "{spaces}{line_str}" )
0 commit comments