| 162 | } |
| 163 | |
| 164 | fn wrap_binders( |
| 165 | &self, |
| 166 | intern: &mut InternTable<M>, |
| 167 | fvars: &[FVarId], |
| 168 | body: KExpr<M>, |
| 169 | as_lambda: bool, |
| 170 | ) -> KExpr<M> { |
| 171 | // Wrap from innermost to outermost: rightmost fvar is the innermost |
| 172 | // binder, so iterate fvars in reverse. |
| 173 | let mut acc = body; |
| 174 | for fv in fvars.iter().rev() { |
| 175 | let decl = self |
| 176 | .find(*fv) |
| 177 | .expect("LocalContext::wrap_binders: fvar not in context"); |
| 178 | acc = match decl { |
| 179 | LocalDecl::CDecl { name, bi, ty } => { |
| 180 | if as_lambda { |
| 181 | intern.intern_expr(KExpr::lam( |
| 182 | name.clone(), |
| 183 | bi.clone(), |
| 184 | ty.clone(), |
| 185 | acc, |
| 186 | )) |
| 187 | } else { |
| 188 | intern.intern_expr(KExpr::all( |
| 189 | name.clone(), |
| 190 | bi.clone(), |
| 191 | ty.clone(), |
| 192 | acc, |
| 193 | )) |
| 194 | } |
| 195 | }, |
| 196 | LocalDecl::LDecl { name, ty, val } => { |
| 197 | // Let-bindings always close as `Let`, regardless of `as_lambda`. |
| 198 | // The `non_dep` flag is conservatively false; refining it would |
| 199 | // require a body-occurrence analysis at close time. |
| 200 | intern.intern_expr(KExpr::let_( |
| 201 | name.clone(), |
| 202 | ty.clone(), |
| 203 | val.clone(), |
| 204 | acc, |
| 205 | false, |
| 206 | )) |
| 207 | }, |
| 208 | }; |
| 209 | } |
| 210 | acc |
| 211 | } |
| 212 | } |
| 213 | |
| 214 | /// Fresh-id generator for [`FVarId`]. One per `TypeChecker`. Counter-based: |