module Accelerator.SM86.RNG.RandomNormal

import Accelerator.SM86.Control
import Accelerator.SM86.Immediate
import Accelerator.SM86.Instruction
import Accelerator.SM86.Program
import Accelerator.SM86.Types

def randomNormalRegister =
  (lambda unrestricted number : Byte .
    (app Accelerator.SM86.Types/sm86Register number))

def randomNormalImmediate =
  (lambda unrestricted b0 : Byte .
    (lambda unrestricted b1 : Byte .
      (lambda unrestricted b2 : Byte .
        (lambda unrestricted b3 : Byte .
          (app Accelerator.SM86.Immediate/sm86Unsigned32 b0 b1 b2 b3)))))

def randomNormalZero =
  (app randomNormalImmediate (byte 0) (byte 0) (byte 0) (byte 0))
def randomNormalThree =
  (app randomNormalImmediate (byte 3) (byte 0) (byte 0) (byte 0))
def randomNormalFour =
  (app randomNormalImmediate (byte 4) (byte 0) (byte 0) (byte 0))
def randomNormalConstantBase =
  (app randomNormalImmediate (byte 40) (byte 0) (byte 0) (byte 0))
def randomNormalOutputPointer =
  (app randomNormalImmediate (byte 96) (byte 1) (byte 0) (byte 0))
def randomNormalSeedScalar =
  (app randomNormalImmediate (byte 144) (byte 1) (byte 0) (byte 0))
def randomNormalCounterScalar =
  (app randomNormalImmediate (byte 148) (byte 1) (byte 0) (byte 0))
def randomNormalScaleScalar =
  (app randomNormalImmediate (byte 152) (byte 1) (byte 0) (byte 0))
def randomNormalMixCounter =
  (app randomNormalImmediate (byte 177) (byte 121) (byte 55) (byte 158))
def randomNormalMix1 =
  (app randomNormalImmediate (byte 107) (byte 202) (byte 235) (byte 133))
def randomNormalMix2 =
  (app randomNormalImmediate (byte 53) (byte 174) (byte 178) (byte 194))
def randomNormalCenter =
  (app randomNormalImmediate (byte 6) (byte 250) (byte 255) (byte 255))

def randomNormalSetBarrier =
  (app
    Accelerator.SM86.Control/sm86SetBarrierControl
    (constructor SM86Barrier SM86Barrier0))
def randomNormalWaitBarrier =
  (app
    Accelerator.SM86.Control/sm86WaitBarrierControl
    (constructor SM86WaitBarrier SM86WaitBarrier0))
def randomNormalPrologueControl : (family SM86Control) =
  (constructor SM86Control SM86ControlValue
    (byte 2)
    (constructor SM86YieldMode SM86Yield)
    (constructor SM86Barrier SM86BarrierNone)
    (constructor SM86Barrier SM86BarrierNone)
    (byte 0) (byte 0))

def randomNormalInstruction =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (app Accelerator.SM86.Program/sm86ProgramSingleton
      (app Accelerator.SM86.Instruction/sm86Instruction body)))

def randomNormalAppend =
  (lambda unrestricted left : (family SM86Program) .
    (lambda unrestricted right : (family SM86Program) .
      (app (app Accelerator.SM86.Program/sm86ProgramAppend left) right)))

def randomNormalPrologue =
  (app randomNormalAppend
    (app randomNormalInstruction
      (constructor SM86InstructionBody SM86MoveConstant
        (app randomNormalRegister (byte 1)) (byte 0)
        randomNormalConstantBase randomNormalPrologueControl))
    (app randomNormalAppend
      (app randomNormalInstruction
        (constructor SM86InstructionBody SM86SpecialToRegister
          (app randomNormalRegister (byte 0))
          (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
          randomNormalSetBarrier))
      (app randomNormalAppend
        (app randomNormalInstruction
          (constructor SM86InstructionBody SM86MoveImmediate
            (app randomNormalRegister (byte 15)) randomNormalFour
            randomNormalWaitBarrier))
        (app randomNormalAppend
          (app randomNormalInstruction
            (constructor SM86InstructionBody SM86SpecialToRegister
              (app randomNormalRegister (byte 18))
              (constructor SM86SpecialRegister SM86ThreadIdX)
              randomNormalSetBarrier))
          (app randomNormalAppend
            (app randomNormalInstruction
              (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant
                (app randomNormalRegister (byte 0))
                (app randomNormalRegister (byte 0))
                (byte 0) randomNormalZero
                (app randomNormalRegister (byte 18)) randomNormalWaitBarrier))
            (app randomNormalAppend
              (app randomNormalInstruction
                (constructor SM86InstructionBody SM86MoveConstant
                  (app randomNormalRegister (byte 6)) (byte 0)
                  randomNormalSeedScalar sm86SafeControl))
              (app randomNormalAppend
                (app randomNormalInstruction
                  (constructor SM86InstructionBody SM86MoveConstant
                    (app randomNormalRegister (byte 7)) (byte 0)
                    randomNormalCounterScalar sm86SafeControl))
                (app randomNormalAppend
                  (app randomNormalInstruction
                    (constructor SM86InstructionBody SM86MoveConstant
                      (app randomNormalRegister (byte 8)) (byte 0)
                      randomNormalScaleScalar sm86SafeControl))
                  (app randomNormalAppend
                    (app randomNormalInstruction
                      (constructor SM86InstructionBody
                        SM86IntegerMultiplyAddImmediate
                        (app randomNormalRegister (byte 2))
                        (app randomNormalRegister (byte 0))
                        randomNormalThree
                        (app randomNormalRegister (byte 7)) sm86SafeControl))
                    (app randomNormalInstruction
                      (constructor SM86InstructionBody SM86MoveImmediate
                        (app randomNormalRegister (byte 9)) randomNormalZero
                        sm86SafeControl)))))))))))

def randomNormalMix =
  (lambda unrestricted shift : Byte .
    (lambda unrestricted multiplier : (family SM86Unsigned32) .
      (app randomNormalAppend
        (app randomNormalInstruction
          (constructor SM86InstructionBody SM86ShiftRightImmediate
            (app randomNormalRegister (byte 5))
            (app randomNormalRegister (byte 4)) shift sm86SafeControl))
        (app randomNormalAppend
          (app randomNormalInstruction
            (constructor SM86InstructionBody SM86LogicThreeInputTruthTable
              (app randomNormalRegister (byte 4))
              (app randomNormalRegister (byte 4))
              (app randomNormalRegister (byte 5)) (byte 60) sm86SafeControl))
          (app randomNormalInstruction
            (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
              (app randomNormalRegister (byte 4))
              (app randomNormalRegister (byte 4)) multiplier
              sm86ZeroRegister sm86SafeControl))))))

def randomNormalByteSum =
  (app randomNormalAppend
    (app randomNormalInstruction
      (constructor SM86InstructionBody SM86ShiftRightImmediate
        (app randomNormalRegister (byte 10))
        (app randomNormalRegister (byte 4)) (byte 8) sm86SafeControl))
    (app randomNormalAppend
      (app randomNormalInstruction
        (constructor SM86InstructionBody SM86ShiftRightImmediate
          (app randomNormalRegister (byte 11))
          (app randomNormalRegister (byte 4)) (byte 16) sm86SafeControl))
      (app randomNormalAppend
        (app randomNormalInstruction
          (constructor SM86InstructionBody SM86ShiftRightImmediate
            (app randomNormalRegister (byte 12))
            (app randomNormalRegister (byte 4)) (byte 24) sm86SafeControl))
        (app randomNormalAppend
          (app randomNormalInstruction
            (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
              (app randomNormalRegister (byte 13))
              (app randomNormalRegister (byte 10))
              (app randomNormalImmediate
                (byte 0) (byte 255) (byte 255) (byte 255))
              (app randomNormalRegister (byte 4)) sm86SafeControl))
          (app randomNormalAppend
            (app randomNormalInstruction
              (constructor SM86InstructionBody SM86IntegerAddThreeRegister
                (app randomNormalRegister (byte 9))
                (app randomNormalRegister (byte 9))
                (app randomNormalRegister (byte 13)) sm86SafeControl))
            (app randomNormalAppend
              (app randomNormalInstruction
                (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
                  (app randomNormalRegister (byte 13))
                  (app randomNormalRegister (byte 11))
                  (app randomNormalImmediate
                    (byte 0) (byte 255) (byte 255) (byte 255))
                  (app randomNormalRegister (byte 10)) sm86SafeControl))
              (app randomNormalAppend
                (app randomNormalInstruction
                  (constructor SM86InstructionBody SM86IntegerAddThreeRegister
                    (app randomNormalRegister (byte 9))
                    (app randomNormalRegister (byte 9))
                    (app randomNormalRegister (byte 13)) sm86SafeControl))
                (app randomNormalAppend
                  (app randomNormalInstruction
                    (constructor SM86InstructionBody
                      SM86IntegerMultiplyAddImmediate
                      (app randomNormalRegister (byte 13))
                      (app randomNormalRegister (byte 12))
                      (app randomNormalImmediate
                        (byte 0) (byte 255) (byte 255) (byte 255))
                      (app randomNormalRegister (byte 11)) sm86SafeControl))
                  (app randomNormalAppend
                    (app randomNormalInstruction
                      (constructor SM86InstructionBody SM86IntegerAddThreeRegister
                        (app randomNormalRegister (byte 9))
                        (app randomNormalRegister (byte 9))
                        (app randomNormalRegister (byte 13)) sm86SafeControl))
                    (app randomNormalInstruction
                      (constructor SM86InstructionBody SM86IntegerAddThreeRegister
                        (app randomNormalRegister (byte 9))
                        (app randomNormalRegister (byte 9))
                        (app randomNormalRegister (byte 12))
                        sm86SafeControl)))))))))))

def randomNormalHash =
  (lambda unrestricted stream : (family SM86Unsigned32) .
    (app randomNormalAppend
      (app randomNormalInstruction
        (constructor SM86InstructionBody SM86IntegerAddThreeImmediate
          (app randomNormalRegister (byte 3))
          (app randomNormalRegister (byte 2)) stream sm86SafeControl))
      (app randomNormalAppend
        (app randomNormalInstruction
          (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate
            (app randomNormalRegister (byte 4))
            (app randomNormalRegister (byte 3)) randomNormalMixCounter
            (app randomNormalRegister (byte 6)) sm86SafeControl))
        (app randomNormalAppend
          (app (app randomNormalMix (byte 16)) randomNormalMix1)
          (app randomNormalAppend
            (app (app randomNormalMix (byte 13)) randomNormalMix2)
            (app randomNormalAppend
              (app randomNormalInstruction
                (constructor SM86InstructionBody SM86ShiftRightImmediate
                  (app randomNormalRegister (byte 5))
                  (app randomNormalRegister (byte 4))
                  (byte 16) sm86SafeControl))
              (app randomNormalAppend
                (app randomNormalInstruction
                  (constructor SM86InstructionBody SM86LogicThreeInputTruthTable
                    (app randomNormalRegister (byte 4))
                    (app randomNormalRegister (byte 4))
                    (app randomNormalRegister (byte 5))
                    (byte 60) sm86SafeControl))
                randomNormalByteSum)))))))

def randomNormalEpilogue =
  (app randomNormalAppend
    (app randomNormalInstruction
      (constructor SM86InstructionBody SM86IntegerAddThreeImmediate
        (app randomNormalRegister (byte 9))
        (app randomNormalRegister (byte 9)) randomNormalCenter
        sm86SafeControl))
    (app randomNormalAppend
      (app randomNormalInstruction
        (constructor SM86InstructionBody SM86IntegerToFloat
          (app randomNormalRegister (byte 14))
          (app randomNormalRegister (byte 9)) sm86SafeControl))
      (app randomNormalAppend
        (app randomNormalInstruction
          (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant
            (app randomNormalRegister (byte 16))
            (app randomNormalRegister (byte 0))
            (app randomNormalRegister (byte 15))
            (byte 0) randomNormalOutputPointer sm86SafeControl))
        (app randomNormalAppend
          (app randomNormalInstruction
            (constructor SM86InstructionBody SM86FloatMultiply
              (app randomNormalRegister (byte 14))
              (app randomNormalRegister (byte 14))
              (app randomNormalRegister (byte 8)) sm86SafeControl))
          (app randomNormalAppend
            (app randomNormalInstruction
              (constructor SM86InstructionBody SM86StoreGlobal
                (app randomNormalRegister (byte 16))
                (app randomNormalRegister (byte 14)) randomNormalZero
                sm86SafeControl))
            (app randomNormalInstruction
              (constructor SM86InstructionBody SM86Exit
                sm86BranchControl)))))))

def randomNormalSM86Program : (family SM86Program) =
  (app randomNormalAppend randomNormalPrologue
    (app randomNormalAppend
      (app randomNormalHash randomNormalZero)
      (app randomNormalAppend
        (app randomNormalHash
          (app randomNormalImmediate (byte 1) (byte 0) (byte 0) (byte 0)))
        (app randomNormalAppend
          (app randomNormalHash
            (app randomNormalImmediate (byte 2) (byte 0) (byte 0) (byte 0)))
          randomNormalEpilogue))))

def randomNormalSM86InstructionCount =
  (app Accelerator.SM86.Program/sm86ProgramCount randomNormalSM86Program)

def randomNormalSM86RegisterCount = (byte-to-nat (byte 24))