Compiler.DependentCore

7856def workReduceAppliedCorePrimitive =
7857  (lambda unrestricted primitive : (family CorePrimitive) .
7858    (lambda unrestricted left : (family CoreTerm) .
7859      (lambda unrestricted right : (family CoreTerm) .
7860        (lambda unrestricted budget : (family NormalizationBudget) .
7861          (eliminate
7862            CorePrimitive
7863            (lambda unrestricted current : (family CorePrimitive) . (family CoreWorkResult))
7864            primitive
7865            (branch
7866              CoreByteEqual
7867              .
7868              (constructor
7869                CoreWorkResult
7870                CoreWorkCompleted
7871                (reduceAppliedCorePrimitive primitive left right)
7872                budget))
7873            (branch
7874              CoreByteLess
7875              .
7876              (constructor
7877                CoreWorkResult
7878                CoreWorkCompleted
7879                (reduceAppliedCorePrimitive primitive left right)
7880                budget))
7881            (branch
7882              CoreNaturalLess
7883              .
7884              (workReduceCorePayloadPair workInspectCoreNatural primitive left right budget))
7885            (branch
7886              CoreNaturalToByte
7887              .
7888              (constructor
7889                CoreWorkResult
7890                CoreWorkCompleted
7891                (reduceAppliedCorePrimitive primitive left right)
7892                budget))
7893            (branch
7894              CoreByteToNatural
7895              .
7896              (constructor
7897                CoreWorkResult
7898                CoreWorkCompleted
7899                (reduceAppliedCorePrimitive primitive left right)
7900                budget))
7901            (branch CoreBytesAppend . (workReduceCoreBytesAppend left right budget))
7902            (branch CoreBytesCons . (workReduceCoreBytesCons left right budget))
7903            (branch
7904              CoreBytesLength
7905              .
7906              (constructor
7907                CoreWorkResult
7908                CoreWorkCompleted
7909                (reduceAppliedCorePrimitive primitive left right)
7910                budget))
7911            (branch
7912              CoreNaturalEliminate
7913              .
7914              (constructor
7915                CoreWorkResult
7916                CoreWorkCompleted
7917                (reduceAppliedCorePrimitive primitive left right)
7918                budget))
7919            (branch
7920              CoreBytesEliminate
7921              .
7922              (constructor
7923                CoreWorkResult
7924                CoreWorkCompleted
7925                (reduceAppliedCorePrimitive primitive left right)
7926                budget))
7927            (branch
7928              CoreBytesEqual
7929              .
7930              (workReduceCorePayloadPair workInspectCoreBytes primitive left right budget))
7931            (branch
7932              CoreFileEffect
7933              .
7934              (constructor
7935                CoreWorkResult
7936                CoreWorkCompleted
7937                (reduceAppliedCorePrimitive primitive left right)
7938                budget))
7939            (branch
7940              CoreEffects
7941              .
7942              (constructor
7943                CoreWorkResult
7944                CoreWorkCompleted
7945                (reduceAppliedCorePrimitive primitive left right)
7946                budget))
7947            (branch
7948              CoreComputation
7949              .
7950              (constructor
7951                CoreWorkResult
7952                CoreWorkCompleted
7953                (reduceAppliedCorePrimitive primitive left right)
7954                budget))
7955            (branch
7956              CoreReturn
7957              .
7958              (constructor
7959                CoreWorkResult
7960                CoreWorkCompleted
7961                (reduceAppliedCorePrimitive primitive left right)
7962                budget))
7963            (branch
7964              CoreBind
7965              .
7966              (constructor
7967                CoreWorkResult
7968                CoreWorkCompleted
7969                (reduceAppliedCorePrimitive primitive left right)
7970                budget))
7971            (branch
7972              CoreReadFile
7973              .
7974              (constructor
7975                CoreWorkResult
7976                CoreWorkCompleted
7977                (reduceAppliedCorePrimitive primitive left right)
7978                budget))
7979            (branch
7980              CoreWriteFile
7981              .
7982              (constructor
7983                CoreWorkResult
7984                CoreWorkCompleted
7985                (reduceAppliedCorePrimitive primitive left right)
7986                budget))
7987            (branch
7988              CoreLinuxOpenNode
7989              .
7990              (constructor
7991                CoreWorkResult
7992                CoreWorkCompleted
7993                (reduceAppliedCorePrimitive primitive left right)
7994                budget))
7995            (branch
7996              CoreLinuxCloseNode
7997              .
7998              (constructor
7999                CoreWorkResult
8000                CoreWorkCompleted
8001                (reduceAppliedCorePrimitive primitive left right)
8002                budget))
8003            (branch
8004              CoreLinuxIoctl
8005              .
8006              (constructor
8007                CoreWorkResult
8008                CoreWorkCompleted
8009                (reduceAppliedCorePrimitive primitive left right)
8010                budget))
8011            (branch
8012              CoreLinuxMmap
8013              .
8014              (constructor
8015                CoreWorkResult
8016                CoreWorkCompleted
8017                (reduceAppliedCorePrimitive primitive left right)
8018                budget))
8019            (branch
8020              CoreLinuxMunmap
8021              .
8022              (constructor
8023                CoreWorkResult
8024                CoreWorkCompleted
8025                (reduceAppliedCorePrimitive primitive left right)
8026                budget))
8027            (branch
8028              CoreBytesSetIndex
8029              .
8030              (constructor
8031                CoreWorkResult
8032                CoreWorkCompleted
8033                (reduceAppliedCorePrimitive primitive left right)
8034                budget))
8035            (branch
8036              CoreBytesIndexNonzero
8037              .
8038              (constructor
8039                CoreWorkResult
8040                CoreWorkCompleted
8041                (reduceAppliedCorePrimitive primitive left right)
8042                budget))
8043            (branch
8044              CoreBytesSetFreeIndex
8045              .
8046              (constructor
8047                CoreWorkResult
8048                CoreWorkCompleted
8049                (reduceAppliedCorePrimitive primitive left right)
8050                budget))
8051            (branch
8052              CoreBytesBuilderType
8053              .
8054              (constructor
8055                CoreWorkResult
8056                CoreWorkCompleted
8057                (reduceAppliedCorePrimitive primitive left right)
8058                budget))
8059            (branch
8060              CoreBytesBuilderEmpty
8061              .
8062              (constructor
8063                CoreWorkResult
8064                CoreWorkCompleted
8065                (reduceAppliedCorePrimitive primitive left right)
8066                budget))
8067            (branch
8068              CoreBytesBuilderChunk
8069              .
8070              (constructor
8071                CoreWorkResult
8072                CoreWorkCompleted
8073                (reduceAppliedCorePrimitive primitive left right)
8074                budget))
8075            (branch
8076              CoreBytesBuilderAppend
8077              .
8078              (constructor
8079                CoreWorkResult
8080                CoreWorkCompleted
8081                (reduceAppliedCorePrimitive primitive left right)
8082                budget))
8083            (branch
8084              CoreBytesBuilderBuild
8085              .
8086              (constructor
8087                CoreWorkResult
8088                CoreWorkCompleted
8089                (reduceAppliedCorePrimitive primitive left right)
8090                budget))
8091            (branch
8092              CoreRuntimeImageV4Build
8093              .
8094              (constructor
8095                CoreWorkResult
8096                CoreWorkCompleted
8097                (reduceAppliedCorePrimitive primitive left right)
8098                budget))
8099            (branch
8100              CoreBytesHead
8101              .
8102              (constructor
8103                CoreWorkResult
8104                CoreWorkCompleted
8105                (reduceAppliedCorePrimitive primitive left right)
8106                budget))
8107            (branch
8108              CoreBytesTail
8109              .
8110              (constructor
8111                CoreWorkResult
8112                CoreWorkCompleted
8113                (reduceAppliedCorePrimitive primitive left right)
8114                budget))
8115            (branch
8116              CoreBytesChecksum
8117              .
8118              (constructor
8119                CoreWorkResult
8120                CoreWorkCompleted
8121                (reduceAppliedCorePrimitive primitive left right)
8122                budget)))))))