search

anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Heap exhausted #96

Closed lukaszcz closed 1 year ago

lukaszcz commented 1 year ago

Seems Geb loops allocating memory on this simple program:

(defpackage #:ho0
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :ho0)

(defparameter *entry*
  (typed
    (app
      (!->
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)))
      (!->
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)))
      (lamb
        (!->
          (coprod
            so1
            so1)
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1)))
        (!->
          (coprod
            so1
            so1)
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1)))
        (index 0))
      (lamb
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1))
        (lamb
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)
          (index 1))))
    (!->
      (coprod
        so1
        so1)
      (!->
        (coprod
          so1
          so1)
        (coprod
          so1
          so1)))))
lukaszcz commented 1 year ago

But this works:

(defpackage #:hoho
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :hoho)

(defparameter *entry*
  (typed
    (lamb
      (coprod
        so1
        so1)
      (!->
        (coprod
          so1
          so1)
        (coprod
          so1
          so1))
      (lamb
        (coprod
          so1
          so1)
        (coprod
          so1
          so1)
        (index 1)))
    (!->
      (coprod
        so1
        so1)
      (!->
        (coprod
          so1
          so1)
        (coprod
          so1
          so1)))))
lukaszcz commented 1 year ago

It seems the problem is passing functions as arguments

lukaszcz commented 1 year ago

I am in fact unable to produce any program using higher-order functions that would be successfully compiled.

mariari commented 1 year ago

I am in fact unable to produce any program using higher-order functions that would be successfully compiled.

Not sure if the situation is changed, but I managed to get it working fine on main

(in-package :cl-user)

(defpackage #:ho0
  (:shadowing-import-from :geb.lambda.spec #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda :geb.common)
  (:export :*entry*))

(in-package :ho0)

(defparameter *entry*
  (app (lamb (!-> (coprod so1 so1) (!-> (coprod so1 so1) (coprod so1 so1)))
             (index 0))
       (lamb
        (!-> (coprod so1 so1) (coprod so1 so1))
        (lamb (coprod so1 so1) (index 1)))))

with the output

GEB-TEST> (lambda:to-circuit nil ho0::*entry* :foo)
def foo x = {
  pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 # 1 # #) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 65536) ((1 * ((mod32 ((# - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 # 1 # #) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * #) + (65536 * #))) + (256 * ((16 * #) + (16 * #))))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * ((# / 18446744073709551616) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (18446744073709551616 * 1)))) 18446744073709551616 ((1 * (((# / 18446744073709551616) / 4294967296) + (mod32 (pwless32 # 1 # #) 1))) / 4294967296) ((1 * ((mod32 (# / 18446744073709551616) 4294967296) + (mod32 (# - 18446744073709551616) 1))) / 4294967296)) + (mod32 (mod32 (4 * (((65536 * #) / 18446744073709551616) + ((mod32 # 16) / 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 18446744073709551616 ((1 * (# + #)) / 4294967296) ((1 * (# + #)) / 4294967296)) + (mod32 (mod32 (4 * (# + #)) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (18446744073709551616 * 1)))) 18446744073709551616 ((1 * ((# / 4294967296) + (mod32 # 1))) / 4294967296) ((1 * ((mod32 # 4294967296) + (mod32 # 1))) / 4294967296)) + (mod32 (mod32 (4 * ((# / 18446744073709551616) + (# / 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 18446744073709551616 ((1 * (# + #)) / 4294967296) ((1 * (# + #)) / 4294967296)) + (mod32 (mod32 (4 * (# + #)) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (4294967296 * 1)))) 1))) / 65536) ((1 * ((mod32 (((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * ((256 * ((16 * #) + (16 * #))) + (256 * ((16 * #) + (16 * #))))) + (65536 * ((256 * ((16 * #) + (16 * #))) + (256 * ((16 * #) + (16 * #))))))) + (256 * ((16 * ((4 * ((# / 4) + (# / 4))) + (4 * ((# / 4) + (# / 4))))) + (16 * ((4 * ((# / 4) + (# / 4))) + (4 * ((# / 4) + (# / 4))))))))) 16) 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 18446744073709551616 ((1 * (# + #)) / 4294967296) ((1 * (# + #)) / 4294967296)) + (mod32 (mod32 (4 * (# + #)) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 1))) / 65536) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * ((256 * #) + (256 * #))) + (65536 * ((256 * #) + (256 * #))))) + (256 * ((16 * ((4 * #) + (4 * #))) + (16 * ((4 * #) + (4 * #))))))) 16) 4))) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (18446744073709551616 * 1)))) 18446744073709551616 ((1 * ((# / 4294967296) + (mod32 # 1))) / 4294967296) ((1 * ((mod32 # 4294967296) + (mod32 # 1))) / 4294967296)) + (mod32 (mod32 (4 * ((# / 18446744073709551616) + (# / 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 18446744073709551616 ((1 * (# + #)) / 4294967296) ((1 * (# + #)) / 4294967296)) + (mod32 (mod32 (4 * (# + #)) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 1))) / 65536) ((1 * ((mod32 (((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * ((256 * (# + #)) + (256 * (# + #)))) + (65536 * ((256 * (# + #)) + (256 * (# + #)))))) + (256 * ((16 * ((4 * (# + #)) + (4 * (# + #)))) + (16 * ((4 * (# + #)) + (4 * (# + #)))))))) 16) 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 18446744073709551616 ((1 * (# + #)) / 4294967296) ((1 * (# + #)) / 4294967296)) + (mod32 (mod32 (4 * (# + #)) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 1))) / 65536) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * ((256 * #) + (256 * #))) + (65536 * ((256 * #) + (256 * #))))) + (256 * ((16 * ((4 * #) + (4 * #))) + (16 * ((4 * #) + (4 * #))))))) 16) 4))) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 18446744073709551616 ((1 * #) / 4294967296) ((1 * #) / 4294967296)) + (mod32 (mod32 (4 * #) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 65536) ((1 * ((mod32 (((pwless32 # 1 # #) - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * (# + #)) + (65536 * (# + #)))) + (256 * ((16 * (# + #)) + (16 * (# + #)))))) 16) 4))) 4) 2))) (1 + 1)) - 1) + (256 * 1)))) 256 ((1 * ((((pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 # 1 # #) / 65536) / 256) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 256) ((1 * ((mod32 ((# - 65536) / 65536) 256) + (mod32 ((pwless32 # 1 # #) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) 2))) (1 + 1)) - 1) + (256 * 1)))) / 256) / 16) + (mod32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 (pwless32 # 1 # #) 18446744073709551616 (# / 4294967296) (# / 4294967296)) + (mod32 (mod32 # 4) 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((((pwless32 # 1 # #) / 4294967296) / 65536) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 65536) ((1 * ((mod32 ((# - 4294967296) / 4294967296) 65536) + (mod32 ((pwless32 # 1 # #) - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * ((65536 * #) + (65536 * #))) + (256 * ((16 * #) + (16 * #))))) 16) 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) (1 + 1)) - 1) + (256 * 1)))) 1))) / 16) ((1 * ((mod32 (((pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 # 1 # #) / 65536) / 256) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 256) ((1 * ((mod32 ((# - 65536) / 65536) 256) + (mod32 ((pwless32 # 1 # #) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 # 1 # #) / 65536) / 256) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 256) ((1 * ((mod32 ((# - 65536) / 65536) 256) + (mod32 ((pwless32 # 1 # #) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) 65536 ((1 * (((# / 65536) / 256) + (mod32 (pwless32 # 1 # #) 1))) / 256) ((1 * ((mod32 (# / 65536) 256) + (mod32 (# - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) 4) 2))) (1 + 1)) - 1) + (256 * 1)))) - 256) / 256) 16) + (mod32 ((pwless32 (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 (pwless32 # 1 # #) 4294967296 (# / 65536) (# / 65536)) + (mod32 (mod32 # 16) 4))) / 65536) + ((mod32 (4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) / (1 + 1))) + (((mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * ((pwless32 # 18446744073709551616 # #) + (mod32 # 2))) (1 + 1)) 1 ((1 * ((2 * #) / (1 + 1))) + (mod32 (2 * (# + #)) (1 + 1))) ((1 * ((2 * #) / (1 + 1))) + (((mod32 # #) - 1) + (4294967296 * 1)))) 4294967296 ((1 * (((# / 4294967296) / 65536) + (mod32 (pwless32 # 1 # #) 1))) / 65536) ((1 * ((mod32 (# / 4294967296) 65536) + (mod32 (# - 4294967296) 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * (# + #)) + (256 * (# + #)))) 16) 4))) 4) 2))) (1 + 1)) 1 ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) / (1 + 1))) + (mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * ((pwless32 # 4294967296 # #) + (mod32 # 4))) / 65536) + ((mod32 (4 * (# + #)) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1))) ((1 * ((2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) / (1 + 1))) + (((mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (65536 * 1)))) 1))) / 256) ((1 * ((mod32 (((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * (# + #)) (1 + 1)) 1 ((1 * (# / #)) + (mod32 (2 * #) (1 + 1))) ((1 * (# / #)) + ((# - 1) + (4294967296 * 1)))) 4294967296 ((1 * ((# / 65536) + (mod32 # 1))) / 65536) ((1 * ((mod32 # 65536) + (mod32 # 1))) / 65536)) + (mod32 (mod32 (65536 * ((4294967296 * #) + (256 * #))) 16) 4))) 4) 2))) (1 + 1))) ((1 * ((2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * (# + #)) / 65536) + ((mod32 (4 * #) 4) / 2))) (1 + 1)) 1 ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1))) ((1 * ((2 * ((# / 65536) + (# / 2))) / (1 + 1))) + (((mod32 (2 * (# + #)) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 (mod32 # #) 1 (# + #) (# + #)) / 65536) / 256) + (mod32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 1))) / 256) ((1 * ((mod32 (((pwless32 # 1 # #) - 65536) / 65536) 256) + (mod32 ((pwless32 (mod32 # #) 1 (# + #) (# + #)) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 (2 * #) (1 + 1)) 1 ((1 * #) + (mod32 # #)) ((1 * #) + (# + #))) 4294967296 ((1 * (# + #)) / 65536) ((1 * (# + #)) / 65536)) + (mod32 (mod32 (65536 * (# + #)) 16) 4))) 4) 2))) / (1 + 1))) + (((mod32 (2 * ((pwless32 (pwless32 (mod32 (2 * (((4 * #) / 65536) + ((mod32 # 4) / 2))) (1 + 1)) 1 ((1 * ((2 * (# + #)) / (1 + 1))) + (mod32 (2 * ((# / 65536) + (# / 2))) (1 + 1))) ((1 * ((2 * (# + #)) / (1 + 1))) + (((mod32 (2 * #) (1 + 1)) - 1) + (65536 * 1)))) 65536 ((1 * ((((pwless32 # 1 # #) / 65536) / 256) + (mod32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 1))) / 256) ((1 * ((mod32 ((# - 65536) / 65536) 256) + (mod32 ((pwless32 # 1 # #) - 65536) 1))) / 256)) + (mod32 (mod32 (4 * ((pwless32 (pwless32 (mod32 # #) 1 (# + #) (# + #)) 4294967296 ((1 * #) / 65536) ((1 * #) / 65536)) + (mod32 (mod32 (65536 * #) 16) 4))) 4) 2))) (1 + 1)) - 1) + (256 * 1)))) - 256) 1))) / 16)
};
GEB-TEST>
mariari commented 1 year ago

I think I see the issue, in the lisp output, it truncates the extra output with # since it goes on too long.

I think the printer itself when it fully tries to render it and dump it, eats too much memory.

Seems the actual output is over 60 MB long, which is a real issue

Note the object in geb format is over 1.5k lines long, and I think my vampir printer tries to format this as it goes and dies in the process

mariari commented 1 year ago

With #97 the issue should be solved, and your circuit should now produce

4 taichi@Gensokyo:~/Documents/Work/Repo/geb/build git:d0804a1:? 1 % ./geb.image -i foo.lisp -e "ho0:*entry*" -l -v           
def bool x = {
  x * (x - 1) = 0;
  x
};
def range31 a = {
  def a0 = bool (fresh ((a \ 1) % 2));
  def a1 = bool (fresh ((a \ 2) % 2));
  def a2 = bool (fresh ((a \ 4) % 2));
  def a3 = bool (fresh ((a \ 8) % 2));
  def a4 = bool (fresh ((a \ 16) % 2));
  def a5 = bool (fresh ((a \ 32) % 2));
  def a6 = bool (fresh ((a \ 64) % 2));
  def a7 = bool (fresh ((a \ 128) % 2));
  def a8 = bool (fresh ((a \ 256) % 2));
  def a9 = bool (fresh ((a \ 512) % 2));
  def a10 = bool (fresh ((a \ 1024) % 2));
  def a11 = bool (fresh ((a \ 2048) % 2));
  def a12 = bool (fresh ((a \ 4096) % 2));
  def a13 = bool (fresh ((a \ 8192) % 2));
  def a14 = bool (fresh ((a \ 16384) % 2));
  def a15 = bool (fresh ((a \ 32768) % 2));
  def a16 = bool (fresh ((a \ 65536) % 2));
  def a17 = bool (fresh ((a \ 131072) % 2));
  def a18 = bool (fresh ((a \ 262144) % 2));
  def a19 = bool (fresh ((a \ 524288) % 2));
  def a20 = bool (fresh ((a \ 1048576) % 2));
  def a21 = bool (fresh ((a \ 2097152) % 2));
  def a22 = bool (fresh ((a \ 4194304) % 2));
  def a23 = bool (fresh ((a \ 8388608) % 2));
  def a24 = bool (fresh ((a \ 16777216) % 2));
  def a25 = bool (fresh ((a \ 33554432) % 2));
  def a26 = bool (fresh ((a \ 67108864) % 2));
  def a27 = bool (fresh ((a \ 134217728) % 2));
  def a28 = bool (fresh ((a \ 268435456) % 2));
  def a29 = bool (fresh ((a \ 536870912) % 2));
  def a30 = bool (fresh ((a \ 1073741824) % 2));
  a = (((((((((((((((((((((((((((((a0 + (2 * a1)) + (4 * a2)) + (8 * a3)) + (16 * a4)) + (32 * a5)) + (64 * a6)) + (128 * a7)) + (256 * a8)) + (512 * a9)) + (1024 * a10)) + (2048 * a11)) + (4096 * a12)) + (8192 * a13)) + (16384 * a14)) + (32768 * a15)) + (65536 * a16)) + (131072 * a17)) + (262144 * a18)) + (524288 * a19)) + (1048576 * a20)) + (2097152 * a21)) + (4194304 * a22)) + (8388608 * a23)) + (16777216 * a24)) + (33554432 * a25)) + (67108864 * a26)) + (134217728 * a27)) + (268435456 * a28)) + (536870912 * a29)) + (1073741824 * a30);
  (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, ())
};
def range32 a = {
  def a0 = bool (fresh ((a \ 1) % 2));
  def a1 = bool (fresh ((a \ 2) % 2));
  def a2 = bool (fresh ((a \ 4) % 2));
  def a3 = bool (fresh ((a \ 8) % 2));
  def a4 = bool (fresh ((a \ 16) % 2));
  def a5 = bool (fresh ((a \ 32) % 2));
  def a6 = bool (fresh ((a \ 64) % 2));
  def a7 = bool (fresh ((a \ 128) % 2));
  def a8 = bool (fresh ((a \ 256) % 2));
  def a9 = bool (fresh ((a \ 512) % 2));
  def a10 = bool (fresh ((a \ 1024) % 2));
  def a11 = bool (fresh ((a \ 2048) % 2));
  def a12 = bool (fresh ((a \ 4096) % 2));
  def a13 = bool (fresh ((a \ 8192) % 2));
  def a14 = bool (fresh ((a \ 16384) % 2));
  def a15 = bool (fresh ((a \ 32768) % 2));
  def a16 = bool (fresh ((a \ 65536) % 2));
  def a17 = bool (fresh ((a \ 131072) % 2));
  def a18 = bool (fresh ((a \ 262144) % 2));
  def a19 = bool (fresh ((a \ 524288) % 2));
  def a20 = bool (fresh ((a \ 1048576) % 2));
  def a21 = bool (fresh ((a \ 2097152) % 2));
  def a22 = bool (fresh ((a \ 4194304) % 2));
  def a23 = bool (fresh ((a \ 8388608) % 2));
  def a24 = bool (fresh ((a \ 16777216) % 2));
  def a25 = bool (fresh ((a \ 33554432) % 2));
  def a26 = bool (fresh ((a \ 67108864) % 2));
  def a27 = bool (fresh ((a \ 134217728) % 2));
  def a28 = bool (fresh ((a \ 268435456) % 2));
  def a29 = bool (fresh ((a \ 536870912) % 2));
  def a30 = bool (fresh ((a \ 1073741824) % 2));
  def a31 = bool (fresh ((a \ 2147483648) % 2));
  a = ((((((((((((((((((((((((((((((a0 + (2 * a1)) + (4 * a2)) + (8 * a3)) + (16 * a4)) + (32 * a5)) + (64 * a6)) + (128 * a7)) + (256 * a8)) + (512 * a9)) + (1024 * a10)) + (2048 * a11)) + (4096 * a12)) + (8192 * a13)) + (16384 * a14)) + (32768 * a15)) + (65536 * a16)) + (131072 * a17)) + (262144 * a18)) + (524288 * a19)) + (1048576 * a20)) + (2097152 * a21)) + (4194304 * a22)) + (8388608 * a23)) + (16777216 * a24)) + (33554432 * a25)) + (67108864 * a26)) + (134217728 * a27)) + (268435456 * a28)) + (536870912 * a29)) + (1073741824 * a30)) + (2147483648 * a31);
  (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, ())
};
def intrange31 a = {
  range31 (a + 1073741824)
};
def intrange32 a = {
  range32 (a + 2147483648)
};
def negative31 a = {
  def (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, ()) =
    intrange31 a;
  a30
};
def negative32 a = {
  def (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, ()) =
    intrange32 a;
  a31
};
def nonnegative32 a = {
  1 - (negative32 a)
};
def less32 a b = {
  intrange31 a;
  intrange31 b;
  negative32 (a - b)
};
def mod32 a b = {
  nonnegative32 b = 0;
  def q = fresh (a \ b);
  def r = fresh (a % b);
  nonnegative32 r = 0;
  a = (b * q) + q;
  less32 r b = 0;
  r
};
def pwmod32 f g x = {
  mod32 (f x) (g x)
};
def pwless32 f g p q = {
  def t = less32 f g;
  ((1 - t) * p) + (t * q)
};
def next_range range a = {
  def a0 = bool (fresh (a % 2));
  def a1 = fresh (a \ 2);
  a = a0 + (2 * a1);
  (a0, range a1)
};
(def g443 x = {
   x
 };
 def g444 x = {
   1 + x
 };
 def g445 x = {
   1 * (x + 0)
 };
 def g446 x = {
   1 * (x / (1 + 1))
 };
 def g447 x = {
   2 + x
 };
 def g448 x = {
   def c486 = x - 1;
   def c487 = mod32 x 1;
   def c488 = x - 1;
   def c489 = mod32 c488 1;
   2 * ((pwless32 x 1 (x / 1) (c486 / 1)) + (pwless32 x 1 c487 (1 + c489)))
 };
 def g449 x = {
   def c490 = x - 2;
   def c491 = mod32 x 1;
   def c492 = x - 2;
   def c493 = mod32 c492 1;
   2 * ((pwless32 x 2 (x / 2) (c490 / 2)) + (pwless32 x 2 c491 (1 + c493)))
 };
 def g450 x = {
   def c494 = x - 4;
   def c495 = mod32 x 1;
   def c496 = x - 4;
   def c497 = mod32 c496 1;
   2 * ((pwless32 x 4 (x / 4) (c494 / 4)) + (pwless32 x 4 c495 (1 + c497)))
 };
 def g451 x = {
   4 + x
 };
 def g452 x = {
   def c498 = x / 2;
   def c499 = x / 2;
   4 * ((c498 / 1) + (2 * ((mod32 c499 2) + (mod32 x 2))))
 };
 def g453 x = {
   mod32 x 1
 };
 def g454 x = {
   x / 2
 };
 def g455 x = {
   mod32 x 4
 };
 def g456 x = {
   x / 8
 };
 def g457 x = {
   x / 16
 };
 def g458 x = {
   x / 256
 };
 def g459 x = {
   x / 65536
 };
 def g460 x = {
   x / 4294967296
 };
 def g461 x = {
   x / 18446744073709551616
 };
 def g462 x = {
   mod32 x (1 + 1)
 };
 def g463 x = {
   def c500 = mod32 x 1;
   c500
 };
 def g464 x = {
   def c501 = mod32 x 1;
   1 + c501
 };
 def g465 x = {
   (1 * (x / (1 + 1))) + (mod32 x (1 + 1))
 };
 def g466 x = {
   def c502 = x - 1;
   def c503 = mod32 x 1;
   def c504 = x - 1;
   def c505 = mod32 c504 1;
   def c506 =
     2 * ((pwless32 x 1 (x / 1) (c502 / 1)) + (pwless32 x 1 c503 (1 + c505)));
   def c507 = 1 * (c506 + 0);
   def c508 = c507;
   def c509 = c508 - 2;
   def c510 = mod32 c508 1;
   def c511 = c508 - 2;
   def c512 = mod32 c511 1;
   def c513 =
     2 * ((pwless32 c508 2 (c508 / 2) (c509 / 2)) + (pwless32 c508 2 c510 (1 + c512)));
   def c514 = c513 / 2;
   def c515 = c513 / 2;
   def c516 = 4 * ((c514 / 1) + (2 * ((mod32 c515 2) + (mod32 c513 2))));
   def c517 = 1 * ((mod32 c516 4) + (c516 / 1));
   def c518 = 1 * (c517 + 0);
   def c519 = c518;
   def c520 = c519 - 4;
   def c521 = mod32 c519 1;
   def c522 = c519 - 4;
   def c523 = mod32 c522 1;
   def c524 =
     2 * ((pwless32 c519 4 (c519 / 4) (c520 / 4)) + (pwless32 c519 4 c521 (1 + c523)));
   def c525 = 4 * ((mod32 c524 2) + (c524 / 4));
   def c526 = mod32 c525 4;
   def c527 = 1 * (c517 + 0);
   def c528 = 4 + c527;
   def c529 = c528 - 4;
   def c530 = mod32 c528 1;
   def c531 = c528 - 4;
   def c532 = mod32 c531 1;
   def c533 =
     2 * ((pwless32 c528 4 (c528 / 4) (c529 / 4)) + (pwless32 c528 4 c530 (1 + c532)));
   def c534 = 4 * ((mod32 c533 2) + (c533 / 4));
   def c535 = mod32 c534 4;
   def c536 = 1 * (c506 + 0);
   def c537 = 2 + c536;
   def c538 = c537 - 2;
   def c539 = mod32 c537 1;
   def c540 = c537 - 2;
   def c541 = mod32 c540 1;
   def c542 =
     2 * ((pwless32 c537 2 (c537 / 2) (c538 / 2)) + (pwless32 c537 2 c539 (1 + c541)));
   def c543 = c542 / 2;
   def c544 = c542 / 2;
   def c545 = 4 * ((c543 / 1) + (2 * ((mod32 c544 2) + (mod32 c542 2))));
   def c546 = 1 * ((mod32 c545 4) + (c545 / 1));
   def c547 = 1 * (c546 + 0);
   def c548 = c547;
   def c549 = c548 - 4;
   def c550 = mod32 c548 1;
   def c551 = c548 - 4;
   def c552 = mod32 c551 1;
   def c553 =
     2 * ((pwless32 c548 4 (c548 / 4) (c549 / 4)) + (pwless32 c548 4 c550 (1 + c552)));
   def c554 = 4 * ((mod32 c553 2) + (c553 / 4));
   def c555 = mod32 c554 4;
   def c556 = 1 * (c546 + 0);
   def c557 = 4 + c556;
   def c558 = c557 - 4;
   def c559 = mod32 c557 1;
   def c560 = c557 - 4;
   def c561 = mod32 c560 1;
   def c562 =
     2 * ((pwless32 c557 4 (c557 / 4) (c558 / 4)) + (pwless32 c557 4 c559 (1 + c561)));
   def c563 = 4 * ((mod32 c562 2) + (c562 / 4));
   def c564 = mod32 c563 4;
   16 * ((4 * ((c526 / 4) + (c535 / 4))) + (4 * ((c555 / 4) + (c564 / 4))))
 };
 def g467 x = {
   def c565 = x - 4;
   def c566 = mod32 x 1;
   def c567 = x - 4;
   def c568 = mod32 c567 1;
   def c569 =
     2 * ((pwless32 x 4 (x / 4) (c565 / 4)) + (pwless32 x 4 c566 (1 + c568)));
   def c570 = 1 * (c569 + 0);
   def c571 = c570;
   def c572 = c571 - 8;
   def c573 = mod32 c571 1;
   def c574 = c571 - 8;
   def c575 = mod32 c574 1;
   def c576 =
     2 * ((pwless32 c571 8 (c571 / 8) (c572 / 8)) + (pwless32 c571 8 c573 (1 + c575)));
   def c577 = c576 / 8;
   def c578 = c576 / 8;
   def c579 = 4 * ((c577 / 4) + (2 * ((mod32 c578 2) + (mod32 c576 2))));
   def c580 = c579 / 4;
   def c581 = c579 / 4;
   def c582 = 16 * ((c580 / 1) + (4 * ((mod32 c581 4) + (mod32 c579 4))));
   def c583 = 1 * ((mod32 c582 16) + (c582 / 1));
   def c584 = 1 * (c569 + 0);
   def c585 = 8 + c584;
   def c586 = c585 - 8;
   def c587 = mod32 c585 1;
   def c588 = c585 - 8;
   def c589 = mod32 c588 1;
   def c590 =
     2 * ((pwless32 c585 8 (c585 / 8) (c586 / 8)) + (pwless32 c585 8 c587 (1 + c589)));
   def c591 = c590 / 8;
   def c592 = c590 / 8;
   def c593 = 4 * ((c591 / 4) + (2 * ((mod32 c592 2) + (mod32 c590 2))));
   def c594 = c593 / 4;
   def c595 = c593 / 4;
   def c596 = 16 * ((c594 / 1) + (4 * ((mod32 c595 4) + (mod32 c593 4))));
   def c597 = 1 * ((mod32 c596 16) + (c596 / 1));
   16 * ((c583 / 16) + (c597 / 16))
 };
 def g468 x = {
   def c598 = x - 1;
   def c599 = mod32 x 1;
   def c600 = x - 1;
   def c601 = mod32 c600 1;
   def c602 =
     2 * ((pwless32 x 1 (x / 1) (c598 / 1)) + (pwless32 x 1 c599 (1 + c601)));
   def c603 = 1 * (c602 + 0);
   def c604 = c603;
   def c605 = c604 - 2;
   def c606 = mod32 c604 1;
   def c607 = c604 - 2;
   def c608 = mod32 c607 1;
   def c609 =
     2 * ((pwless32 c604 2 (c604 / 2) (c605 / 2)) + (pwless32 c604 2 c606 (1 + c608)));
   def c610 = c609 / 2;
   def c611 = c609 / 2;
   def c612 = 4 * ((c610 / 1) + (2 * ((mod32 c611 2) + (mod32 c609 2))));
   def c613 = 1 * (c612 + 0);
   def c614 = c613;
   def c615 = c614 - 4;
   def c616 = mod32 c614 1;
   def c617 = c614 - 4;
   def c618 = mod32 c617 1;
   def c619 =
     2 * ((pwless32 c614 4 (c614 / 4) (c615 / 4)) + (pwless32 c614 4 c616 (1 + c618)));
   def c620 = 1 * (c619 + 0);
   def c621 = c620;
   def c622 = c621 - 8;
   def c623 = mod32 c621 1;
   def c624 = c621 - 8;
   def c625 = mod32 c624 1;
   def c626 =
     2 * ((pwless32 c621 8 (c621 / 8) (c622 / 8)) + (pwless32 c621 8 c623 (1 + c625)));
   def c627 = c626 / 8;
   def c628 = c626 / 8;
   def c629 = 4 * ((c627 / 4) + (2 * ((mod32 c628 2) + (mod32 c626 2))));
   def c630 = c629 / 4;
   def c631 = c629 / 4;
   def c632 = 16 * ((c630 / 1) + (4 * ((mod32 c631 4) + (mod32 c629 4))));
   def c633 = 1 * ((mod32 c632 16) + (c632 / 1));
   def c634 = 1 * (c619 + 0);
   def c635 = 8 + c634;
   def c636 = c635 - 8;
   def c637 = mod32 c635 1;
   def c638 = c635 - 8;
   def c639 = mod32 c638 1;
   def c640 =
     2 * ((pwless32 c635 8 (c635 / 8) (c636 / 8)) + (pwless32 c635 8 c637 (1 + c639)));
   def c641 = c640 / 8;
   def c642 = c640 / 8;
   def c643 = 4 * ((c641 / 4) + (2 * ((mod32 c642 2) + (mod32 c640 2))));
   def c644 = c643 / 4;
   def c645 = c643 / 4;
   def c646 = 16 * ((c644 / 1) + (4 * ((mod32 c645 4) + (mod32 c643 4))));
   def c647 = 1 * ((mod32 c646 16) + (c646 / 1));
   def c648 = 1 * (c612 + 0);
   def c649 = 4 + c648;
   def c650 = c649 - 4;
   def c651 = mod32 c649 1;
   def c652 = c649 - 4;
   def c653 = mod32 c652 1;
   def c654 =
     2 * ((pwless32 c649 4 (c649 / 4) (c650 / 4)) + (pwless32 c649 4 c651 (1 + c653)));
   def c655 = 1 * (c654 + 0);
   def c656 = c655;
   def c657 = c656 - 8;
   def c658 = mod32 c656 1;
   def c659 = c656 - 8;
   def c660 = mod32 c659 1;
   def c661 =
     2 * ((pwless32 c656 8 (c656 / 8) (c657 / 8)) + (pwless32 c656 8 c658 (1 + c660)));
   def c662 = c661 / 8;
   def c663 = c661 / 8;
   def c664 = 4 * ((c662 / 4) + (2 * ((mod32 c663 2) + (mod32 c661 2))));
   def c665 = c664 / 4;
   def c666 = c664 / 4;
   def c667 = 16 * ((c665 / 1) + (4 * ((mod32 c666 4) + (mod32 c664 4))));
   def c668 = 1 * ((mod32 c667 16) + (c667 / 1));
   def c669 = 1 * (c654 + 0);
   def c670 = 8 + c669;
   def c671 = c670 - 8;
   def c672 = mod32 c670 1;
   def c673 = c670 - 8;
   def c674 = mod32 c673 1;
   def c675 =
     2 * ((pwless32 c670 8 (c670 / 8) (c671 / 8)) + (pwless32 c670 8 c672 (1 + c674)));
   def c676 = c675 / 8;
   def c677 = c675 / 8;
   def c678 = 4 * ((c676 / 4) + (2 * ((mod32 c677 2) + (mod32 c675 2))));
   def c679 = c678 / 4;
   def c680 = c678 / 4;
   def c681 = 16 * ((c679 / 1) + (4 * ((mod32 c680 4) + (mod32 c678 4))));
   def c682 = 1 * ((mod32 c681 16) + (c681 / 1));
   def c683 = 1 * (c602 + 0);
   def c684 = 2 + c683;
   def c685 = c684 - 2;
   def c686 = mod32 c684 1;
   def c687 = c684 - 2;
   def c688 = mod32 c687 1;
   def c689 =
     2 * ((pwless32 c684 2 (c684 / 2) (c685 / 2)) + (pwless32 c684 2 c686 (1 + c688)));
   def c690 = c689 / 2;
   def c691 = c689 / 2;
   def c692 = 4 * ((c690 / 1) + (2 * ((mod32 c691 2) + (mod32 c689 2))));
   def c693 = 1 * (c692 + 0);
   def c694 = c693;
   def c695 = c694 - 4;
   def c696 = mod32 c694 1;
   def c697 = c694 - 4;
   def c698 = mod32 c697 1;
   def c699 =
     2 * ((pwless32 c694 4 (c694 / 4) (c695 / 4)) + (pwless32 c694 4 c696 (1 + c698)));
   def c700 = 1 * (c699 + 0);
   def c701 = c700;
   def c702 = c701 - 8;
   def c703 = mod32 c701 1;
   def c704 = c701 - 8;
   def c705 = mod32 c704 1;
   def c706 =
     2 * ((pwless32 c701 8 (c701 / 8) (c702 / 8)) + (pwless32 c701 8 c703 (1 + c705)));
   def c707 = c706 / 8;
   def c708 = c706 / 8;
   def c709 = 4 * ((c707 / 4) + (2 * ((mod32 c708 2) + (mod32 c706 2))));
   def c710 = c709 / 4;
   def c711 = c709 / 4;
   def c712 = 16 * ((c710 / 1) + (4 * ((mod32 c711 4) + (mod32 c709 4))));
   def c713 = 1 * ((mod32 c712 16) + (c712 / 1));
   def c714 = 1 * (c699 + 0);
   def c715 = 8 + c714;
   def c716 = c715 - 8;
   def c717 = mod32 c715 1;
   def c718 = c715 - 8;
   def c719 = mod32 c718 1;
   def c720 =
     2 * ((pwless32 c715 8 (c715 / 8) (c716 / 8)) + (pwless32 c715 8 c717 (1 + c719)));
   def c721 = c720 / 8;
   def c722 = c720 / 8;
   def c723 = 4 * ((c721 / 4) + (2 * ((mod32 c722 2) + (mod32 c720 2))));
   def c724 = c723 / 4;
   def c725 = c723 / 4;
   def c726 = 16 * ((c724 / 1) + (4 * ((mod32 c725 4) + (mod32 c723 4))));
   def c727 = 1 * ((mod32 c726 16) + (c726 / 1));
   def c728 = 1 * (c692 + 0);
   def c729 = 4 + c728;
   def c730 = c729 - 4;
   def c731 = mod32 c729 1;
   def c732 = c729 - 4;
   def c733 = mod32 c732 1;
   def c734 =
     2 * ((pwless32 c729 4 (c729 / 4) (c730 / 4)) + (pwless32 c729 4 c731 (1 + c733)));
   def c735 = 1 * (c734 + 0);
   def c736 = c735;
   def c737 = c736 - 8;
   def c738 = mod32 c736 1;
   def c739 = c736 - 8;
   def c740 = mod32 c739 1;
   def c741 =
     2 * ((pwless32 c736 8 (c736 / 8) (c737 / 8)) + (pwless32 c736 8 c738 (1 + c740)));
   def c742 = c741 / 8;
   def c743 = c741 / 8;
   def c744 = 4 * ((c742 / 4) + (2 * ((mod32 c743 2) + (mod32 c741 2))));
   def c745 = c744 / 4;
   def c746 = c744 / 4;
   def c747 = 16 * ((c745 / 1) + (4 * ((mod32 c746 4) + (mod32 c744 4))));
   def c748 = 1 * ((mod32 c747 16) + (c747 / 1));
   def c749 = 1 * (c734 + 0);
   def c750 = 8 + c749;
   def c751 = c750 - 8;
   def c752 = mod32 c750 1;
   def c753 = c750 - 8;
   def c754 = mod32 c753 1;
   def c755 =
     2 * ((pwless32 c750 8 (c750 / 8) (c751 / 8)) + (pwless32 c750 8 c752 (1 + c754)));
   def c756 = c755 / 8;
   def c757 = c755 / 8;
   def c758 = 4 * ((c756 / 4) + (2 * ((mod32 c757 2) + (mod32 c755 2))));
   def c759 = c758 / 4;
   def c760 = c758 / 4;
   def c761 = 16 * ((c759 / 1) + (4 * ((mod32 c760 4) + (mod32 c758 4))));
   def c762 = 1 * ((mod32 c761 16) + (c761 / 1));
   65536 * ((256 * ((16 * ((c633 / 16) + (c647 / 16))) + (16 * ((c668 / 16) + (c682 / 16))))) + (256 * ((16 * ((c713 / 16) + (c727 / 16))) + (16 * ((c748 / 16) + (c762 / 16))))))
 };
 def g469 x = {
   def c763 = x / 2;
   mod32 c763 2
 };
 def g470 x = {
   def c764 = mod32 x 4;
   c764 / 2
 };
 def g471 x = {
   def c765 = x / 4;
   mod32 c765 4
 };
 def g472 x = {
   def c766 = mod32 x 16;
   c766 / 4
 };
 def g473 x = {
   def c767 = x / 256;
   def c768 = 1 * ((c767 / 16) + (mod32 x 1));
   c768 / 16
 };
 def g474 x = {
   def c769 = x / 65536;
   def c770 = 1 * ((c769 / 256) + (mod32 x 1));
   c770 / 256
 };
 def g475 x = {
   def c771 = x / 4294967296;
   def c772 = 1 * ((c771 / 65536) + (mod32 x 1));
   c772 / 65536
 };
 def g476 x = {
   def c773 = x / 18446744073709551616;
   def c774 = 1 * ((c773 / 4294967296) + (mod32 x 1));
   c774 / 4294967296
 };
 def g477 x = {
   (mod32 x (1 + 1)) - 1
 };
 def g478 x = {
   def c775 = x - 2;
   def c776 = mod32 x 1;
   def c777 = x - 2;
   def c778 = mod32 c777 1;
   def c779 =
     2 * ((pwless32 x 2 (x / 2) (c775 / 2)) + (pwless32 x 2 c776 (1 + c778)));
   def c780 = c779 / 2;
   def c781 = c779 / 2;
   def c782 = 4 * ((c780 / 1) + (2 * ((mod32 c781 2) + (mod32 c779 2))));
   def c783 = 1 * (c782 + 0);
   def c784 = c783;
   def c785 = c784 - 4;
   def c786 = mod32 c784 1;
   def c787 = c784 - 4;
   def c788 = mod32 c787 1;
   def c789 =
     2 * ((pwless32 c784 4 (c784 / 4) (c785 / 4)) + (pwless32 c784 4 c786 (1 + c788)));
   def c790 = 1 * (c789 + 0);
   def c791 = c790;
   def c792 = c791 - 8;
   def c793 = mod32 c791 1;
   def c794 = c791 - 8;
   def c795 = mod32 c794 1;
   def c796 =
     2 * ((pwless32 c791 8 (c791 / 8) (c792 / 8)) + (pwless32 c791 8 c793 (1 + c795)));
   def c797 = c796 / 8;
   def c798 = c796 / 8;
   def c799 = 4 * ((c797 / 4) + (2 * ((mod32 c798 2) + (mod32 c796 2))));
   def c800 = c799 / 4;
   def c801 = c799 / 4;
   def c802 = 16 * ((c800 / 1) + (4 * ((mod32 c801 4) + (mod32 c799 4))));
   def c803 = 1 * ((mod32 c802 16) + (c802 / 1));
   def c804 = 1 * (c789 + 0);
   def c805 = 8 + c804;
   def c806 = c805 - 8;
   def c807 = mod32 c805 1;
   def c808 = c805 - 8;
   def c809 = mod32 c808 1;
   def c810 =
     2 * ((pwless32 c805 8 (c805 / 8) (c806 / 8)) + (pwless32 c805 8 c807 (1 + c809)));
   def c811 = c810 / 8;
   def c812 = c810 / 8;
   def c813 = 4 * ((c811 / 4) + (2 * ((mod32 c812 2) + (mod32 c810 2))));
   def c814 = c813 / 4;
   def c815 = c813 / 4;
   def c816 = 16 * ((c814 / 1) + (4 * ((mod32 c815 4) + (mod32 c813 4))));
   def c817 = 1 * ((mod32 c816 16) + (c816 / 1));
   def c818 = 1 * (c782 + 0);
   def c819 = 4 + c818;
   def c820 = c819 - 4;
   def c821 = mod32 c819 1;
   def c822 = c819 - 4;
   def c823 = mod32 c822 1;
   def c824 =
     2 * ((pwless32 c819 4 (c819 / 4) (c820 / 4)) + (pwless32 c819 4 c821 (1 + c823)));
   def c825 = 1 * (c824 + 0);
   def c826 = c825;
   def c827 = c826 - 8;
   def c828 = mod32 c826 1;
   def c829 = c826 - 8;
   def c830 = mod32 c829 1;
   def c831 =
     2 * ((pwless32 c826 8 (c826 / 8) (c827 / 8)) + (pwless32 c826 8 c828 (1 + c830)));
   def c832 = c831 / 8;
   def c833 = c831 / 8;
   def c834 = 4 * ((c832 / 4) + (2 * ((mod32 c833 2) + (mod32 c831 2))));
   def c835 = c834 / 4;
   def c836 = c834 / 4;
   def c837 = 16 * ((c835 / 1) + (4 * ((mod32 c836 4) + (mod32 c834 4))));
   def c838 = 1 * ((mod32 c837 16) + (c837 / 1));
   def c839 = 1 * (c824 + 0);
   def c840 = 8 + c839;
   def c841 = c840 - 8;
   def c842 = mod32 c840 1;
   def c843 = c840 - 8;
   def c844 = mod32 c843 1;
   def c845 =
     2 * ((pwless32 c840 8 (c840 / 8) (c841 / 8)) + (pwless32 c840 8 c842 (1 + c844)));
   def c846 = c845 / 8;
   def c847 = c845 / 8;
   def c848 = 4 * ((c846 / 4) + (2 * ((mod32 c847 2) + (mod32 c845 2))));
   def c849 = c848 / 4;
   def c850 = c848 / 4;
   def c851 = 16 * ((c849 / 1) + (4 * ((mod32 c850 4) + (mod32 c848 4))));
   def c852 = 1 * ((mod32 c851 16) + (c851 / 1));
   256 * ((16 * ((c803 / 16) + (c817 / 16))) + (16 * ((c838 / 16) + (c852 / 16))))
 };
 def g479 x = {
   def c853 = x - 2;
   def c854 = mod32 x 1;
   def c855 = x - 2;
   def c856 = mod32 c855 1;
   def c857 =
     2 * ((pwless32 x 2 (x / 2) (c853 / 2)) + (pwless32 x 2 c854 (1 + c856)));
   def c858 = c857 / 2;
   def c859 = c857 / 2;
   def c860 = 4 * ((c858 / 1) + (2 * ((mod32 c859 2) + (mod32 c857 2))));
   def c861 = 1 * ((mod32 c860 4) + (c860 / 1));
   def c862 = 1 * (c861 + 0);
   def c863 = c862;
   def c864 = c863 - 4;
   def c865 = mod32 c863 1;
   def c866 = c863 - 4;
   def c867 = mod32 c866 1;
   def c868 =
     2 * ((pwless32 c863 4 (c863 / 4) (c864 / 4)) + (pwless32 c863 4 c865 (1 + c867)));
   def c869 = 4 * ((mod32 c868 2) + (c868 / 4));
   def c870 = mod32 c869 4;
   def c871 = 1 * (c861 + 0);
   def c872 = 4 + c871;
   def c873 = c872 - 4;
   def c874 = mod32 c872 1;
   def c875 = c872 - 4;
   def c876 = mod32 c875 1;
   def c877 =
     2 * ((pwless32 c872 4 (c872 / 4) (c873 / 4)) + (pwless32 c872 4 c874 (1 + c876)));
   def c878 = 4 * ((mod32 c877 2) + (c877 / 4));
   def c879 = mod32 c878 4;
   4 * ((c870 / 4) + (c879 / 4))
 };
 def g480 x = {
   def c880 = x - 4;
   def c881 = mod32 x 1;
   def c882 = x - 4;
   def c883 = mod32 c882 1;
   def c884 =
     2 * ((pwless32 x 4 (x / 4) (c880 / 4)) + (pwless32 x 4 c881 (1 + c883)));
   def c885 = 4 * ((mod32 c884 2) + (c884 / 4));
   def c886 = mod32 c885 4;
   c886 / 4
 };
 def g481 x = {
   def c887 = x - 8;
   def c888 = mod32 x 1;
   def c889 = x - 8;
   def c890 = mod32 c889 1;
   def c891 =
     2 * ((pwless32 x 8 (x / 8) (c887 / 8)) + (pwless32 x 8 c888 (1 + c890)));
   def c892 = c891 / 8;
   def c893 = c891 / 8;
   def c894 = 4 * ((c892 / 4) + (2 * ((mod32 c893 2) + (mod32 c891 2))));
   def c895 = c894 / 4;
   def c896 = c894 / 4;
   def c897 = 16 * ((c895 / 1) + (4 * ((mod32 c896 4) + (mod32 c894 4))));
   def c898 = 1 * ((mod32 c897 16) + (c897 / 1));
   c898 / 16
 };
 def entry x = {
   def c899 = g445 x;
   def c900 = c899;
   def c901 = g445 x;
   def c902 = g444 c901;
   def c903 = g445 x;
   def c904 = c903;
   def c905 = g445 x;
   def c906 = g444 c905;
   def c907 =
     65536 * ((4294967296 * ((g468 c900) + (g468 c902))) + (256 * ((g466 c904) + (g466 c906))));
   def c908 = 4 * ((g461 c907) + (g472 c907));
   def c909 = 2 * ((g461 c908) + (g470 c908));
   def c910 =
     pwless32 (g462 c909) 1 (g465 c909) ((g446 c909) + ((g477 c909) + (18446744073709551616 * 1)));
   def c911 = g461 c910;
   def c912 =
     2 * ((pwless32 c910 18446744073709551616 (g476 c910) (g476 c911)) + (g470 c908));
   def c913 =
     pwless32 (g462 c912) 1 (g465 c912) ((g446 c912) + ((g477 c912) + (4294967296 * 1)));
   def c914 = g460 c913;
   def c915 =
     4 * ((pwless32 c913 4294967296 (g475 c913) (g475 c914)) + (g472 c907));
   def c916 = 2 * ((g459 c915) + (g470 c915));
   def c917 =
     pwless32 (g462 c916) 1 (g465 c916) ((g446 c916) + ((g477 c916) + (65536 * 1)));
   def c918 = g459 c917;
   def c919 = 2 * ((pwless32 c917 65536 (g474 c917) (g474 c918)) + (g470 c915));
   def c920 =
     pwless32 (g462 c919) 1 (g465 c919) ((g446 c919) + ((g477 c919) + (256 * 1)));
   def c921 = g458 c920;
   pwless32 c920 256 (g473 c920) (g473 c921)
 };)%
lukaszcz commented 1 year ago

That's better, but still quite large for such a simple lambda-term.

rokopt commented 1 year ago

That's better, but still quite large for such a simple lambda-term.

Indeed! #89 is what we need to do to make this sane.

rokopt commented 1 year ago

Can this be closed as fixed by #97 (with #115 having also greatly reduced the size of the polynomial produced by this STLC term)?