module Accelerator.SM86.Program

import Accelerator.SM86.Instruction
import Accelerator.SM86.Control
import Accelerator.SM86.Immediate
import Accelerator.SM86.InstructionEncoding
import Accelerator.SM86.Types
import Std.Natural

def sm86ProgramEmpty : (family SM86Program) =
  (constructor SM86Program SM86ProgramEnd)

def sm86ProgramSingleton =
  (lambda unrestricted instruction : (family SM86Instruction) .
    (constructor SM86Program SM86ProgramNext instruction (constructor SM86Program SM86ProgramEnd)))

def sm86ProgramAppend =
  (lambda unrestricted left : (family SM86Program) .
    (eliminate
      SM86Program
      (lambda unrestricted value : (family SM86Program) .
        (pi unrestricted right : (family SM86Program) . (family SM86Program)))
      left
      (branch SM86ProgramEnd . (lambda unrestricted right : (family SM86Program) . right))
      (branch
        SM86ProgramNext
        head
        tail
        ih_tail
        .
        (lambda unrestricted right : (family SM86Program) .
          (constructor SM86Program SM86ProgramNext head (ih_tail right))))))

def sm86ProgramCount =
  (lambda unrestricted program : (family SM86Program) .
    (eliminate
      SM86Program
      (lambda unrestricted value : (family SM86Program) . Nat)
      program
      (branch SM86ProgramEnd . zero)
      (branch SM86ProgramNext head tail ih_tail . (succ ih_tail))))

-- A backward branch whose displacement is derived from the body it repeats.
-- The descriptor is the SM86 BRA ABI; the caller owns the predicate and
-- must ensure its loop variable advances before the branch.  The branch is
-- relative to its successor, so it crosses the body and itself.
def sm86ProgramLoopWhileNot =
  (lambda unrestricted predicate : (family SM86Predicate) .
    (lambda unrestricted body :
      (pi unrestricted tail : (family SM86Program) . (family SM86Program)) .
      (lambda erased admitted :
        (equal Nat
          (naturalLess
            (naturalMultiply sm86InstructionBytes
              (succ (sm86ProgramCount (body sm86ProgramEmpty))))
            2147483648) 1) .
        (lambda unrestricted tail : (family SM86Program) .
          (let unrestricted distance =
            (succ (sm86ProgramCount (body sm86ProgramEmpty))) in
          (body
            (constructor SM86Program SM86ProgramNext
              (sm86NegatedPredicatedInstruction predicate
                (constructor SM86InstructionBody SM86Branch
                  (sm86Unsigned32FromNaturalTruncated
                    (naturalSaturatingSubtract 4294967296 (naturalMultiply sm86InstructionBytes distance)))
                  (sm86Unsigned32 (byte 255) (byte 255) (byte 131) (byte 3))
                  sm86BranchControl))
              tail)))))))