module Accelerator.SM86.HalfFormat

import Accelerator.SM86.Instruction
import Accelerator.SM86.Program
import Std.Natural

-- A program moved to another 16-bit format: every instruction that makes,
-- reads or multiplies halves -- F2FP (the pack), the widening (HADD2.F32 /
-- PRMT) and HMMA -- replaced by its twin in the format, every other
-- instruction kept.  Halves are made and read only by those three (the
-- model has no other half arithmetic), and moved as bits by the rest (loads,
-- stores, LDSM, shuffles), so a program whose halves are all its own -- none
-- read from or written for another program in the other format -- computes
-- the same thing with its halves in the new format.  A system moves its
-- images together (Coppelius.Build.DeviceImages).
def sm86BodyInBFloat16 =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86InstructionBody))
      body
      (branch SM86MoveConstant destination bank offset control . (constructor SM86InstructionBody SM86MoveConstant destination bank offset control))
      (branch SM86SpecialToRegister destination source control . (constructor SM86InstructionBody SM86SpecialToRegister destination source control))
      (branch SM86MoveImmediate destination immediate control . (constructor SM86InstructionBody SM86MoveImmediate destination immediate control))
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant destination left bank offset addend control))
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate destination left immediate addend control))
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant destination left right bank offset control))
      (branch SM86IntegerAddThreeImmediate destination left immediate control . (constructor SM86InstructionBody SM86IntegerAddThreeImmediate destination left immediate control))
      (branch SM86IntegerAddThreeRegister destination left right control . (constructor SM86InstructionBody SM86IntegerAddThreeRegister destination left right control))
      (branch SM86ShiftRightImmediate destination source amount control . (constructor SM86InstructionBody SM86ShiftRightImmediate destination source amount control))
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (constructor SM86InstructionBody SM86LogicThreeInputTruthTable destination left right truthTable control))
      (branch SM86IntegerToFloat destination source control . (constructor SM86InstructionBody SM86IntegerToFloat destination source control))
      (branch SM86FloatAdd destination left right control . (constructor SM86InstructionBody SM86FloatAdd destination left right control))
      (branch SM86FloatMultiply destination left right control . (constructor SM86InstructionBody SM86FloatMultiply destination left right control))
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd destination left right addend control))
      (branch SM86MultiFunctionUnitApproximation destination source operation control . (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation destination source operation control))
      (branch SM86FloatMinimumOrMaximum destination left right mode control . (constructor SM86InstructionBody SM86FloatMinimumOrMaximum destination left right mode control))
      (branch SM86FloatNegate destination source control . (constructor SM86InstructionBody SM86FloatNegate destination source control))
      (branch SM86FloatPairToPackedHalfPair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low control))
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low control))
      (branch SM86HalfToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector control))
      (branch SM86BFloat16ToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector control))
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control))
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control))
      (branch SM86LoadGlobal destination address offset control . (constructor SM86InstructionBody SM86LoadGlobal destination address offset control))
      (branch SM86LoadGlobalWide destination address offset control . (constructor SM86InstructionBody SM86LoadGlobalWide destination address offset control))
      (branch SM86WarpShuffle destination source lane segment mode control . (constructor SM86InstructionBody SM86WarpShuffle destination source lane segment mode control))
      (branch SM86LoadShared destination address offset control . (constructor SM86InstructionBody SM86LoadShared destination address offset control))
      (branch SM86LoadSharedMatrix destination address offset count transpose control . (constructor SM86InstructionBody SM86LoadSharedMatrix destination address offset count transpose control))
      (branch SM86StoreShared address value offset control . (constructor SM86InstructionBody SM86StoreShared address value offset control))
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (constructor SM86InstructionBody SM86LoadGlobalToShared address offset source sourceOffset control))
      (branch SM86CommitAsyncGroup control . (constructor SM86InstructionBody SM86CommitAsyncGroup control))
      (branch SM86WaitAsyncGroups count control . (constructor SM86InstructionBody SM86WaitAsyncGroups count control))
      (branch SM86BarrierSynchronize control . (constructor SM86InstructionBody SM86BarrierSynchronize control))
      (branch SM86StoreGlobal address value offset control . (constructor SM86InstructionBody SM86StoreGlobal address value offset control))
      (branch SM86StoreGlobalWide address value offset control . (constructor SM86InstructionBody SM86StoreGlobalWide address value offset control))
      (branch SM86StoreGlobal64 address value offset control . (constructor SM86InstructionBody SM86StoreGlobal64 address value offset control))
      (branch SM86ReduceGlobalAddFloat32 address value offset control . (constructor SM86InstructionBody SM86ReduceGlobalAddFloat32 address value offset control))
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate predicate source immediate control))
      (branch SM86Branch offset descriptor control . (constructor SM86InstructionBody SM86Branch offset descriptor control))
      (branch SM86Exit control . (constructor SM86InstructionBody SM86Exit control))))

def sm86BodyWithHalfFormat =
  (lambda unrestricted format : (family SM86HalfFormat) .
    (lambda unrestricted body : (family SM86InstructionBody) .
      (eliminate SM86HalfFormat (lambda unrestricted current : (family SM86HalfFormat) . (family SM86InstructionBody)) format
        (branch SM86Binary16 . body)
        (branch SM86BFloat16 . (sm86BodyInBFloat16 body)))))

def sm86InstructionWithHalfFormat =
  (lambda unrestricted format : (family SM86HalfFormat) .
    (lambda unrestricted instruction : (family SM86Instruction) .
      (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family SM86Instruction)) instruction
        (branch SM86InstructionValue guard body .
          (constructor SM86Instruction SM86InstructionValue guard (sm86BodyWithHalfFormat format body))))))

def sm86ProgramWithHalfFormat =
  (lambda unrestricted format : (family SM86HalfFormat) .
    (lambda unrestricted program : (family SM86Program) .
      (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . (family SM86Program)) program
        (branch SM86ProgramEnd . (constructor SM86Program SM86ProgramEnd))
        (branch SM86ProgramNext instruction rest induction .
          (constructor SM86Program SM86ProgramNext (sm86InstructionWithHalfFormat format instruction) induction)))))

-- 1 for an instruction that makes, reads or multiplies binary16 halves
def sm86BodyIsBinary16 =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . Nat)
      body
      (branch SM86MoveConstant destination bank offset control . 0)
      (branch SM86SpecialToRegister destination source control . 0)
      (branch SM86MoveImmediate destination immediate control . 0)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 0)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 0)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 0)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . 0)
      (branch SM86IntegerAddThreeRegister destination left right control . 0)
      (branch SM86ShiftRightImmediate destination source amount control . 0)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 0)
      (branch SM86IntegerToFloat destination source control . 0)
      (branch SM86FloatAdd destination left right control . 0)
      (branch SM86FloatMultiply destination left right control . 0)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 0)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . 0)
      (branch SM86FloatNegate destination source control . 0)
      (branch SM86FloatPairToPackedHalfPair destination high low control . 1)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 0)
      (branch SM86HalfToFloat destination source selector control . 1)
      (branch SM86BFloat16ToFloat destination source selector control . 0)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 1)
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 0)
      (branch SM86LoadGlobal destination address offset control . 0)
      (branch SM86LoadGlobalWide destination address offset control . 0)
      (branch SM86WarpShuffle destination source lane segment mode control . 0)
      (branch SM86LoadShared destination address offset control . 0)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
      (branch SM86StoreShared address value offset control . 0)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
      (branch SM86CommitAsyncGroup control . 0)
      (branch SM86WaitAsyncGroups count control . 0)
      (branch SM86BarrierSynchronize control . 0)
      (branch SM86StoreGlobal address value offset control . 0)
      (branch SM86StoreGlobalWide address value offset control . 0)
      (branch SM86StoreGlobal64 address value offset control . 0)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 0)
      (branch SM86Branch offset descriptor control . 0)
      (branch SM86Exit control . 0)))

-- 1 for one that makes, reads or multiplies bfloat16 halves
def sm86BodyIsBFloat16 =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (eliminate SM86InstructionBody
      (lambda unrestricted current : (family SM86InstructionBody) . Nat)
      body
      (branch SM86MoveConstant destination bank offset control . 0)
      (branch SM86SpecialToRegister destination source control . 0)
      (branch SM86MoveImmediate destination immediate control . 0)
      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 0)
      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 0)
      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 0)
      (branch SM86IntegerAddThreeImmediate destination left immediate control . 0)
      (branch SM86IntegerAddThreeRegister destination left right control . 0)
      (branch SM86ShiftRightImmediate destination source amount control . 0)
      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 0)
      (branch SM86IntegerToFloat destination source control . 0)
      (branch SM86FloatAdd destination left right control . 0)
      (branch SM86FloatMultiply destination left right control . 0)
      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 0)
      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
      (branch SM86FloatMinimumOrMaximum destination left right mode control . 0)
      (branch SM86FloatNegate destination source control . 0)
      (branch SM86FloatPairToPackedHalfPair destination high low control . 0)
      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 1)
      (branch SM86HalfToFloat destination source selector control . 0)
      (branch SM86BFloat16ToFloat destination source selector control . 1)
      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 0)
      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 1)
      (branch SM86LoadGlobal destination address offset control . 0)
      (branch SM86LoadGlobalWide destination address offset control . 0)
      (branch SM86WarpShuffle destination source lane segment mode control . 0)
      (branch SM86LoadShared destination address offset control . 0)
      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
      (branch SM86StoreShared address value offset control . 0)
      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
      (branch SM86CommitAsyncGroup control . 0)
      (branch SM86WaitAsyncGroups count control . 0)
      (branch SM86BarrierSynchronize control . 0)
      (branch SM86StoreGlobal address value offset control . 0)
      (branch SM86StoreGlobalWide address value offset control . 0)
      (branch SM86StoreGlobal64 address value offset control . 0)
      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 0)
      (branch SM86Branch offset descriptor control . 0)
      (branch SM86Exit control . 0)))

-- how many of a program's instructions are of a format's
def sm86ProgramCountOf =
  (lambda unrestricted of : (pi unrestricted body : (family SM86InstructionBody) . Nat) .
    (lambda unrestricted program : (family SM86Program) .
      (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . Nat) program
        (branch SM86ProgramEnd . 0)
        (branch SM86ProgramNext instruction rest induction .
          (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . Nat) instruction
            (branch SM86InstructionValue guard body . (naturalAdd (of body) induction)))))))

def sm86ProgramBinary16Count = (sm86ProgramCountOf sm86BodyIsBinary16)
def sm86ProgramBFloat16Count = (sm86ProgramCountOf sm86BodyIsBFloat16)