Source/Packages

Compiler.MachineX86NativeOffset

packages/compiler/src/Compiler/MachineX86NativeOffset.alpha

584 lines46 declarations23.5 KiBSHA-256 89175cb5d529

def · lines 188–268

x86NativeSubtractUnsigned32

Full file
188def x86NativeSubtractUnsigned32 :
189  (pi unrestricted left : (family X86NativeUnsigned32) .
190    (pi unrestricted right : (family X86NativeUnsigned32) .
191      (family X86NativeUnsigned32SubtractResult))) =
192  (lambda unrestricted left : (family X86NativeUnsigned32) .
193    (lambda unrestricted right : (family X86NativeUnsigned32) .
194      (eliminate
195        X86NativeUnsigned32
196        (lambda unrestricted leftValue : (family X86NativeUnsigned32) .
197          (family X86NativeUnsigned32SubtractResult))
198        left
199        (branch
200          X86NativeUnsigned32Value
201          left0
202          left1
203          left2
204          left3
205          .
206          (eliminate
207            X86NativeUnsigned32
208            (lambda unrestricted rightValue : (family X86NativeUnsigned32) .
209              (family X86NativeUnsigned32SubtractResult))
210            right
211            (branch
212              X86NativeUnsigned32Value
213              right0
214              right1
215              right2
216              right3
217              .
218              (eliminate
219                X86NativeByteSubtractResult
220                (lambda unrestricted result0 : (family X86NativeByteSubtractResult) .
221                  (family X86NativeUnsigned32SubtractResult))
222                (x86NativeSubtractByte left0 right0 zero)
223                (branch
224                  X86NativeByteSubtractValue
225                  difference0
226                  borrow1
227                  .
228                  (eliminate
229                    X86NativeByteSubtractResult
230                    (lambda unrestricted result1 : (family X86NativeByteSubtractResult) .
231                      (family X86NativeUnsigned32SubtractResult))
232                    (x86NativeSubtractByte left1 right1 borrow1)
233                    (branch
234                      X86NativeByteSubtractValue
235                      difference1
236                      borrow2
237                      .
238                      (eliminate
239                        X86NativeByteSubtractResult
240                        (lambda unrestricted result2 : (family X86NativeByteSubtractResult) .
241                          (family X86NativeUnsigned32SubtractResult))
242                        (x86NativeSubtractByte left2 right2 borrow2)
243                        (branch
244                          X86NativeByteSubtractValue
245                          difference2
246                          borrow3
247                          .
248                          (eliminate
249                            X86NativeByteSubtractResult
250                            (lambda unrestricted result3 : (family X86NativeByteSubtractResult) .
251                              (family X86NativeUnsigned32SubtractResult))
252                            (x86NativeSubtractByte left3 right3 borrow3)
253                            (branch
254                              X86NativeByteSubtractValue
255                              difference3
256                              finalBorrow
257                              .
258                              (constructor
259                                X86NativeUnsigned32SubtractResult
260                                X86NativeUnsigned32SubtractValue
261                                (constructor
262                                  X86NativeUnsigned32
263                                  X86NativeUnsigned32Value
264                                  difference0
265                                  difference1
266                                  difference2
267                                  difference3)
268                                finalBorrow)))))))))))))))

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.