356 | | cc[[C]] = lam_n C_CC , if C_CC exists |
357 | | and has arity n |
358 | | cc[[x::t]] = x_CC , if x_CC exists |
359 | | = to iso<t> x , otherwise |
360 | | cc[[lit]] = lit |
361 | | cc[[e1 e2]] = cc[[e1]] $: cc[e2] |
362 | | cc[[e1@t]] = cc[[e1]]@t^ |
363 | | cc[[\x -> e]] = lam_1 $ \x -> cc[e]] |
364 | | cc[let x = e1 in e2] = let x = cc[[e1]] in cc[[e2]] |
365 | | cc[[ |
| 362 | cc[[C]] = $WC_CC |
| 363 | cc[[x::t]] |
| 364 | | if x_CC exists = x_CC |
| 365 | | otherwise = to iso<t> x |
| 366 | cc[[lit]] = lit |
| 367 | cc[[e1 e2]] = cc[[e1]] $: cc[e2] |
| 368 | cc[[e1@t]] = cc[[e1]]@t^ |
| 369 | cc[[\x -> e]] = lam_1 $ \x_CC -> cc[e]] |
| 370 | cc[let x = e1 in e2] = let x_CC = cc[[e1]] in cc[[e2]] |
| 371 | cc[[case e x::t of alts]]= case cc[[e]] x_CC::t^ |
| 372 | of cc[[alts]] |
| 373 | cc[[e `cast` t]] = cc[[e]] `cast` t^ |
| 374 | |
| 375 | cc[[alt1; ..; altn]] = cc[[alt1]]; ..; cc[altn]] |
| 376 | cc[[default -> e]] = default -> cc[[e]] |
| 377 | cc[[C x1 .. xn -> e]] |
| 378 | | if C_CC exists = C_CC x1_CC .. xn_CC -> cc[[e]] |
| 379 | | otherwise = C x1 .. xn -> cc[[e]] |
372 | | turns an `n`-ary function into an `n`-ary closure. (NB: This is not the same as `to iso` for that type, as we do not change the types of the arguments of the function.) |
373 | | |
374 | | ---- |
375 | | chak: revision front |
376 | | ---- |
377 | | |
378 | | Apart from the standard rules, we need to handle the following special cases: |
379 | | * We come across a value variable `v` where `idCC v == NoCC` whose type is `t`: we generate `convert t v` (see below). |
380 | | * We come across a case expression where the scrutinised type `T` has `tyConCC T == NoCC`: we leave the case expression as is (i.e., unconverted), but make sure that the `idCC` field of all variables bound by patterns in the alternatives have their `idCC` field as `NoCC`. (This implies that the previous case will kick in and convert the (unconverted) values obtained after decomposition.) |
381 | | * Whenever we have an FC `cast` from or to a newtype `T`, where `tyConCC T == NoCC`, we need to add a `convert tau` or `trevnoc tau`, respectively. We can spot these casts by inspecting the kind of every coercion used in a cast. One side of the equality will have the newtype constructor. |
382 | | * We come across a dfun: If its `idCC` field is `NoCC`, we keep the selection as is, but apply `convert t e` from it, where `t` is the type of the selected method and `e` the selection expression. If `idCC` is `ConvCC d_CC`, and the dfun's class is converted, `d_CC` is fully converted. If it's class is not converted, we also keep the selection unconverted, but have a bit less to do in `convert t e`. '''TODO:''' This needs to be fully worked out. |
| 386 | turns an `n`-ary function into an `n`-ary closure. (NB: This is not the same as `to iso` for that type, as we do not convert the types of the arguments of the function.) |