@@ -82,23 +82,26 @@ fn seq_preconds(fcx: fn_ctxt, pps: [pre_and_post]) -> precond {
82
82
83
83
fn seq_preconds_go ( fcx : fn_ctxt , pps : [ pre_and_post ] , first : pre_and_post )
84
84
-> precond {
85
- let sz: uint = vec:: len ( pps) ;
86
- if sz >= 1 u {
87
- let second = pps[ 0 ] ;
88
- assert ( pps_len ( second) == num_constraints ( fcx. enclosing ) ) ;
89
- let second_pre = clone ( second. precondition ) ;
90
- difference ( second_pre, first. postcondition ) ;
91
- let next_first = clone ( first. precondition ) ;
92
- union ( next_first, second_pre) ;
93
- let next_first_post = clone ( first. postcondition ) ;
94
- seq_tritv ( next_first_post, second. postcondition ) ;
95
- ret seq_preconds_go ( fcx, vec:: slice ( pps, 1 u, sz) ,
96
- @{ precondition: next_first,
97
- postcondition: next_first_post} ) ;
98
- } else { ret first. precondition ; }
85
+ let mut pps = pps;
86
+ let mut first = first;
87
+ loop {
88
+ let sz: uint = vec:: len ( pps) ;
89
+ if sz >= 1 u {
90
+ let second = pps[ 0 ] ;
91
+ assert ( pps_len ( second) == num_constraints ( fcx. enclosing ) ) ;
92
+ let second_pre = clone ( second. precondition ) ;
93
+ difference ( second_pre, first. postcondition ) ;
94
+ let next_first = clone ( first. precondition ) ;
95
+ union ( next_first, second_pre) ;
96
+ let next_first_post = clone ( first. postcondition ) ;
97
+ seq_tritv ( next_first_post, second. postcondition ) ;
98
+ pps = vec:: slice ( pps, 1 u, sz) ;
99
+ first = @{ precondition: next_first,
100
+ postcondition: next_first_post} ;
101
+ } else { ret first. precondition ; }
102
+ }
99
103
}
100
104
101
-
102
105
if sz >= 1 u {
103
106
let first = pps[ 0 ] ;
104
107
assert ( pps_len ( first) == num_vars) ;
0 commit comments