10043def workReduceCoreGenericEliminator =
10044 (lambda unrestricted familyName : Bytes .
10045 (lambda unrestricted motive : (family CoreTerm) .
10046 (lambda unrestricted scrutinee : (family CoreTerm) .
10047 (lambda unrestricted branches : (family CoreTerm) .
10048 (eliminate
10049 CoreTerm
10050 (lambda unrestricted current : (family CoreTerm) .
10051 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))
10052 scrutinee
10053 (branch
10054 CoreUniverse
10055 level
10056 .
10057 (lambda unrestricted budget : (family NormalizationBudget) .
10058 (coreWorkCharge
10059 coreWorkOne
10060 budget
10061 (lambda unrestricted remaining : (family NormalizationBudget) .
10062 (constructor
10063 CoreWorkResult
10064 CoreWorkCompleted
10065 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10066 remaining)))))
10067 (branch
10068 CoreNatural
10069 .
10070 (lambda unrestricted budget : (family NormalizationBudget) .
10071 (coreWorkCharge
10072 coreWorkOne
10073 budget
10074 (lambda unrestricted remaining : (family NormalizationBudget) .
10075 (constructor
10076 CoreWorkResult
10077 CoreWorkCompleted
10078 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10079 remaining)))))
10080 (branch
10081 CoreNaturalLiteral
10082 value
10083 .
10084 (lambda unrestricted budget : (family NormalizationBudget) .
10085 (coreWorkCharge
10086 coreWorkOne
10087 budget
10088 (lambda unrestricted remaining : (family NormalizationBudget) .
10089 (constructor
10090 CoreWorkResult
10091 CoreWorkCompleted
10092 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10093 remaining)))))
10094 (branch
10095 CoreBound
10096 index
10097 .
10098 (lambda unrestricted budget : (family NormalizationBudget) .
10099 (coreWorkCharge
10100 coreWorkOne
10101 budget
10102 (lambda unrestricted remaining : (family NormalizationBudget) .
10103 (constructor
10104 CoreWorkResult
10105 CoreWorkCompleted
10106 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10107 remaining)))))
10108 (branch
10109 CorePi
10110 multiplicity
10111 domain
10112 codomain
10113 ih_domain
10114 ih_codomain
10115 .
10116 (lambda unrestricted budget : (family NormalizationBudget) .
10117 (coreWorkCharge
10118 coreWorkOne
10119 budget
10120 (lambda unrestricted remaining : (family NormalizationBudget) .
10121 (constructor
10122 CoreWorkResult
10123 CoreWorkCompleted
10124 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10125 remaining)))))
10126 (branch
10127 CoreLambda
10128 multiplicity
10129 domain
10130 body
10131 ih_domain
10132 ih_body
10133 .
10134 (lambda unrestricted budget : (family NormalizationBudget) .
10135 (coreWorkCharge
10136 coreWorkOne
10137 budget
10138 (lambda unrestricted remaining : (family NormalizationBudget) .
10139 (constructor
10140 CoreWorkResult
10141 CoreWorkCompleted
10142 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10143 remaining)))))
10144 (branch
10145 CoreLet
10146 multiplicity
10147 annotation
10148 value
10149 body
10150 ih_annotation
10151 ih_value
10152 ih_body
10153 .
10154 (lambda unrestricted budget : (family NormalizationBudget) .
10155 (coreWorkCharge
10156 coreWorkOne
10157 budget
10158 (lambda unrestricted remaining : (family NormalizationBudget) .
10159 (coreWorkBind
10160 (ih_value remaining)
10161 (lambda unrestricted newValue : (family CoreTerm) .
10162 (lambda unrestricted afterValue : (family NormalizationBudget) .
10163 (coreWorkBind
10164 (ih_body afterValue)
10165 (lambda unrestricted newBody : (family CoreTerm) .
10166 (lambda unrestricted afterBody : (family NormalizationBudget) .
10167 (workSubstituteCoreTop newValue newBody afterBody)))))))))))
10168 (branch
10169 CoreApplication
10170 function
10171 argument
10172 ih_function
10173 ih_argument
10174 .
10175 (lambda unrestricted budget : (family NormalizationBudget) .
10176 (coreWorkCharge
10177 coreWorkOne
10178 budget
10179 (lambda unrestricted remaining : (family NormalizationBudget) .
10180 (constructor
10181 CoreWorkResult
10182 CoreWorkCompleted
10183 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10184 remaining)))))
10185 (branch
10186 CoreNaturalArithmetic
10187 operation
10188 function
10189 argument
10190 ih_function
10191 ih_argument
10192 .
10193 (lambda unrestricted budget : (family NormalizationBudget) .
10194 (coreWorkCharge
10195 coreWorkOne
10196 budget
10197 (lambda unrestricted remaining : (family NormalizationBudget) .
10198 (constructor
10199 CoreWorkResult
10200 CoreWorkCompleted
10201 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10202 remaining)))))
10203 (branch
10204 CoreNaturalSuccessor
10205 predecessor
10206 ih_predecessor
10207 .
10208 (lambda unrestricted budget : (family NormalizationBudget) .
10209 (coreWorkCharge
10210 coreWorkOne
10211 budget
10212 (lambda unrestricted remaining : (family NormalizationBudget) .
10213 (constructor
10214 CoreWorkResult
10215 CoreWorkCompleted
10216 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10217 remaining)))))
10218 (branch
10219 CoreByte
10220 .
10221 (lambda unrestricted budget : (family NormalizationBudget) .
10222 (coreWorkCharge
10223 coreWorkOne
10224 budget
10225 (lambda unrestricted remaining : (family NormalizationBudget) .
10226 (constructor
10227 CoreWorkResult
10228 CoreWorkCompleted
10229 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10230 remaining)))))
10231 (branch
10232 CoreByteLiteral
10233 value
10234 .
10235 (lambda unrestricted budget : (family NormalizationBudget) .
10236 (coreWorkCharge
10237 coreWorkOne
10238 budget
10239 (lambda unrestricted remaining : (family NormalizationBudget) .
10240 (constructor
10241 CoreWorkResult
10242 CoreWorkCompleted
10243 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10244 remaining)))))
10245 (branch
10246 CoreBytes
10247 .
10248 (lambda unrestricted budget : (family NormalizationBudget) .
10249 (coreWorkCharge
10250 coreWorkOne
10251 budget
10252 (lambda unrestricted remaining : (family NormalizationBudget) .
10253 (constructor
10254 CoreWorkResult
10255 CoreWorkCompleted
10256 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10257 remaining)))))
10258 (branch
10259 CoreBytesLiteral
10260 value
10261 .
10262 (lambda unrestricted budget : (family NormalizationBudget) .
10263 (coreWorkCharge
10264 coreWorkOne
10265 budget
10266 (lambda unrestricted remaining : (family NormalizationBudget) .
10267 (constructor
10268 CoreWorkResult
10269 CoreWorkCompleted
10270 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10271 remaining)))))
10272 (branch
10273 CorePrimitiveTerm
10274 primitive
10275 .
10276 (lambda unrestricted budget : (family NormalizationBudget) .
10277 (coreWorkCharge
10278 coreWorkOne
10279 budget
10280 (lambda unrestricted remaining : (family NormalizationBudget) .
10281 (constructor
10282 CoreWorkResult
10283 CoreWorkCompleted
10284 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10285 remaining)))))
10286 (branch
10287 CoreTermSequenceEnd
10288 .
10289 (lambda unrestricted budget : (family NormalizationBudget) .
10290 (coreWorkCharge
10291 coreWorkOne
10292 budget
10293 (lambda unrestricted remaining : (family NormalizationBudget) .
10294 (constructor
10295 CoreWorkResult
10296 CoreWorkCompleted
10297 (constructor CoreTerm CoreTermSequenceEnd)
10298 remaining)))))
10299 (branch
10300 CoreTermSequenceNext
10301 head
10302 tail
10303 ih_head
10304 ih_tail
10305 .
10306 (lambda unrestricted budget : (family NormalizationBudget) .
10307 (coreWorkCharge
10308 coreWorkOne
10309 budget
10310 (lambda unrestricted remaining : (family NormalizationBudget) .
10311 (coreWorkBind
10312 (ih_head remaining)
10313 (lambda unrestricted newHead : (family CoreTerm) .
10314 (lambda unrestricted afterHead : (family NormalizationBudget) .
10315 (coreWorkBind
10316 (ih_tail afterHead)
10317 (lambda unrestricted newTail : (family CoreTerm) .
10318 (lambda unrestricted afterTail : (family NormalizationBudget) .
10319 (constructor
10320 CoreWorkResult
10321 CoreWorkCompleted
10322 (constructor CoreTerm CoreTermSequenceNext newHead newTail)
10323 afterTail)))))))))))
10324 (branch
10325 CoreFamilyApplication
10326 constructorFamily
10327 arguments
10328 ih_arguments
10329 .
10330 (lambda unrestricted budget : (family NormalizationBudget) .
10331 (coreWorkCharge
10332 coreWorkOne
10333 budget
10334 (lambda unrestricted remaining : (family NormalizationBudget) .
10335 (constructor
10336 CoreWorkResult
10337 CoreWorkCompleted
10338 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10339 remaining)))))
10340 (branch
10341 CoreConstructorApplication
10342 constructorFamily
10343 constructorName
10344 arguments
10345 ih_arguments
10346 .
10347 (lambda unrestricted budget : (family NormalizationBudget) .
10348 (coreWorkCharge
10349 coreWorkOne
10350 budget
10351 (lambda unrestricted remaining : (family NormalizationBudget) .
10352 (coreWorkChargeBytes
10353 familyName
10354 remaining
10355 (lambda unrestricted afterName : (family NormalizationBudget) .
10356 (coreWorkChargeBytes
10357 constructorFamily
10358 afterName
10359 (lambda unrestricted afterFamily : (family NormalizationBudget) .
10360 (coreWorkChoose
10361 (bytes-equal familyName constructorFamily)
10362 (lambda unrestricted force : Nat .
10363 (workFindCoreEliminatorBranch
10364 constructorName
10365 branches
10366 (lambda unrestricted selection : (family CoreEliminatorBranchSelection) .
10367 (lambda unrestricted afterSelection : (family NormalizationBudget) .
10368 (coreWorkBind
10369 (ih_arguments afterSelection)
10370 (lambda unrestricted candidates : (family CoreTerm) .
10371 (lambda unrestricted afterArguments : (family NormalizationBudget) .
10372 (workFinishCoreEliminatorReduction
10373 familyName
10374 motive
10375 scrutinee
10376 branches
10377 arguments
10378 candidates
10379 selection
10380 afterArguments))))))
10381 afterFamily))
10382 (lambda unrestricted force : Nat .
10383 (constructor
10384 CoreWorkResult
10385 CoreWorkCompleted
10386 (constructor
10387 CoreTerm
10388 CoreEliminator
10389 familyName
10390 motive
10391 scrutinee
10392 branches)
10393 afterFamily)))))))))))
10394 (branch
10395 CoreEliminatorBranch
10396 constructorName
10397 binderCount
10398 body
10399 ih_body
10400 .
10401 (lambda unrestricted budget : (family NormalizationBudget) .
10402 (coreWorkCharge
10403 coreWorkOne
10404 budget
10405 (lambda unrestricted remaining : (family NormalizationBudget) .
10406 (constructor
10407 CoreWorkResult
10408 CoreWorkCompleted
10409 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10410 remaining)))))
10411 (branch
10412 CoreEliminator
10413 nestedFamily
10414 nestedMotive
10415 nestedScrutinee
10416 nestedBranches
10417 ih_motive
10418 ih_scrutinee
10419 ih_branches
10420 .
10421 (lambda unrestricted budget : (family NormalizationBudget) .
10422 (coreWorkCharge
10423 coreWorkOne
10424 budget
10425 (lambda unrestricted remaining : (family NormalizationBudget) .
10426 (constructor
10427 CoreWorkResult
10428 CoreWorkCompleted
10429 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10430 remaining))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.