1102def livenessPlaceOne =
1103 (lambda unrestricted arenaBytes : (family ModelWord64) .
1104 (lambda unrestricted lifetime : (family Lifetime) .
1105 (lambda unrestricted state : (family LivenessPlacementState) .
1106 (eliminate
1107 LivenessPlacementState
1108 (lambda unrestricted current : (family LivenessPlacementState) .
1109 (family LivenessPlacementStep))
1110 state
1111 (branch
1112 LivenessPlacementStateValue
1113 peak
1114 slots
1115 placements
1116 reused
1117 fresh
1118 .
1119 (eliminate
1120 Lifetime
1121 (lambda unrestricted current : (family Lifetime) . (family LivenessPlacementStep))
1122 lifetime
1123 (branch
1124 LifetimeValue
1125 tensor
1126 firstUse
1127 lastUse
1128 bytes
1129 alignment
1130 .
1131 (eliminate
1132 LivenessOptionalSlot
1133 (lambda unrestricted current : (family LivenessOptionalSlot) .
1134 (family LivenessPlacementStep))
1135 (livenessBestReusable lifetime slots)
1136 (branch
1137 LivenessNoSlot
1138 .
1139 (eliminate
1140 ModelWord64CheckedResult
1141 (lambda unrestricted result : (family ModelWord64CheckedResult) .
1142 (family LivenessPlacementStep))
1143 (livenessAlignUp (stdByteCountValue peak) (stdByteAlignmentValue alignment))
1144 (branch
1145 ModelWord64CheckedSucceeded
1146 offset
1147 .
1148 (eliminate
1149 ModelWord64CheckedResult
1150 (lambda unrestricted result : (family ModelWord64CheckedResult) .
1151 (family LivenessPlacementStep))
1152 (modelWord64AddChecked offset (stdByteCountValue bytes))
1153 (branch
1154 ModelWord64CheckedSucceeded
1155 end
1156 .
1157 (nat-eliminate
1158 (lambda unrestricted outside : Nat . (family LivenessPlacementStep))
1159 (constructor
1160 LivenessPlacementStep
1161 LivenessPlacementAdvanced
1162 (constructor
1163 LivenessPlacementState
1164 LivenessPlacementStateValue
1165 (stdByteCount end)
1166 (constructor
1167 LivenessSlots
1168 LivenessSlotsNext
1169 (constructor
1170 LivenessSlot
1171 LivenessSlotValue
1172 (stdByteCount offset)
1173 bytes
1174 lastUse)
1175 slots)
1176 (constructor
1177 Placements
1178 PlacementsNext
1179 (constructor
1180 Placement
1181 PlacementValue
1182 lifetime
1183 (stdByteCount offset)
1184 bytes)
1185 placements)
1186 reused
1187 (succ fresh)))
1188 (lambda unrestricted predecessor : Nat .
1189 (lambda unrestricted induction : (family LivenessPlacementStep) .
1190 (constructor
1191 LivenessPlacementStep
1192 LivenessPlacementStopped
1193 (constructor LivenessErrorCode PlacementArenaExhausted)
1194 state)))
1195 (modelWord64LessThan arenaBytes end)))
1196 (branch
1197 ModelWord64CheckedFailed
1198 error
1199 .
1200 (constructor
1201 LivenessPlacementStep
1202 LivenessPlacementStopped
1203 (constructor LivenessErrorCode PlacementArithmeticOverflow)
1204 state))))
1205 (branch
1206 ModelWord64CheckedFailed
1207 error
1208 .
1209 (constructor
1210 LivenessPlacementStep
1211 LivenessPlacementStopped
1212 (constructor LivenessErrorCode PlacementArithmeticOverflow)
1213 state))))
1214 (branch
1215 LivenessSomeSlot
1216 selected
1217 .
1218 (eliminate
1219 LivenessSlot
1220 (lambda unrestricted current : (family LivenessSlot) .
1221 (family LivenessPlacementStep))
1222 selected
1223 (branch
1224 LivenessSlotValue
1225 offset
1226 capacity
1227 previousLastUse
1228 .
1229 (constructor
1230 LivenessPlacementStep
1231 LivenessPlacementAdvanced
1232 (constructor
1233 LivenessPlacementState
1234 LivenessPlacementStateValue
1235 peak
1236 (livenessReplaceSlot
1237 selected
1238 (constructor LivenessSlot LivenessSlotValue offset capacity lastUse)
1239 slots)
1240 (constructor
1241 Placements
1242 PlacementsNext
1243 (constructor Placement PlacementValue lifetime offset capacity)
1244 placements)
1245 (succ reused)
1246 fresh)))))))))))))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.