Accelerator.SM86.Program

1module Accelerator.SM86.Program
2
3import Accelerator.SM86.Instruction
4import Accelerator.SM86.Control
5import Accelerator.SM86.Immediate
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Types
8import Std.Natural
9
10def sm86ProgramEmpty : (family SM86Program) =
11  (constructor SM86Program SM86ProgramEnd)
12
13def sm86ProgramSingleton =
14  (lambda unrestricted instruction : (family SM86Instruction) .
15    (constructor SM86Program SM86ProgramNext instruction (constructor SM86Program SM86ProgramEnd)))
16
17def sm86ProgramAppend =
18  (lambda unrestricted left : (family SM86Program) .
19    (eliminate
20      SM86Program
21      (lambda unrestricted value : (family SM86Program) .
22        (pi unrestricted right : (family SM86Program) . (family SM86Program)))
23      left
24      (branch SM86ProgramEnd . (lambda unrestricted right : (family SM86Program) . right))
25      (branch
26        SM86ProgramNext
27        head
28        tail
29        ih_tail
30        .
31        (lambda unrestricted right : (family SM86Program) .
32          (constructor SM86Program SM86ProgramNext head (ih_tail right))))))
33
34def sm86ProgramCount =
35  (lambda unrestricted program : (family SM86Program) .
36    (eliminate
37      SM86Program
38      (lambda unrestricted value : (family SM86Program) . Nat)
39      program
40      (branch SM86ProgramEnd . zero)
41      (branch SM86ProgramNext head tail ih_tail . (succ ih_tail))))
42
43-- A backward branch whose displacement is derived from the body it repeats.
44-- The descriptor is the SM86 BRA ABI; the caller owns the predicate and
45-- must ensure its loop variable advances before the branch.  The branch is
46-- relative to its successor, so it crosses the body and itself.
47def sm86ProgramLoopWhileNot =
48  (lambda unrestricted predicate : (family SM86Predicate) .
49    (lambda unrestricted body :
50      (pi unrestricted tail : (family SM86Program) . (family SM86Program)) .
51      (lambda erased admitted :
52        (equal Nat
53          (naturalLess
54            (naturalMultiply sm86InstructionBytes
55              (succ (sm86ProgramCount (body sm86ProgramEmpty))))
56            2147483648) 1) .
57        (lambda unrestricted tail : (family SM86Program) .
58          (let unrestricted distance =
59            (succ (sm86ProgramCount (body sm86ProgramEmpty))) in
60          (body
61            (constructor SM86Program SM86ProgramNext
62              (sm86NegatedPredicatedInstruction predicate
63                (constructor SM86InstructionBody SM86Branch
64                  (sm86Unsigned32FromNaturalTruncated
65                    (naturalSaturatingSubtract 4294967296 (naturalMultiply sm86InstructionBytes distance)))
66                  (sm86Unsigned32 (byte 255) (byte 255) (byte 131) (byte 3))
67                  sm86BranchControl))
68              tail)))))))