(* The transducer of Definitions 5.1 and 5.2: the step of SUBLEQ_A of Host.v followed by the device on the
   top words, and the programs P and P* of Constructions 6.8 and 6.11 moved to 2^A words. *)
From Stdlib Require Import List Bool Arith Lia.
Import ListNotations.
From TH Require Import Host.

Section Dev.
Variable A : nat.

(* the device cells, the halt address and the variables of the programs *)
Definition cwr : nat := SW A - 7.
Definition ceot : nat := SW A - 6.
Definition crw : nat := SW A - 5.
Definition crd : nat := SW A - 4.
Definition rin : nat := SW A - 3.
Definition rout : nat := SW A - 2.
Definition haltc : nat := SW A - 1.
Definition zc : nat := SW A - 16.
Definition onec : nat := SW A - 15.
Definition t1c : nat := SW A - 14.
Definition t2c : nat := SW A - 13.
Definition neg1c : nat := SW A - 12.
Definition eokc : nat := SW A - 11.

Definition setm (s : hst) (c v : nat) : hst :=
  mkH (hpc s) (hhalt s) (map (fun j => if Nat.eqb j c then v else memv s j) (seq 0 (SW A))).

(* a byte read into R_in, its sign bit copied into the bits above the eighth *)
Definition sext (v : nat) : nat := if v <? 128 then v else v + SW A - 256.

(* the tape, the head and the output word, with two records of the run: whether a byte was requested at
   the end of the tape before any rewind, and the heads at which rewinds were requested *)
Record dev := mkD { dtape : list nat; dhead : nat; dout : list nat; dlate : bool; drew : list nat }.

Definition device (s : hst) (d : dev) : hst * dev :=
  let wr := Nat.eqb (memv s cwr) 1 in
  let rd := Nat.eqb (memv s crd) 1 in
  let rw := Nat.eqb (memv s crw) 1 in
  let ok := dhead d <? length (dtape d) in
  let s1 := if wr then setm s rout 0 else s in
  let s2 := if rd then (if ok then setm (setm s1 rin (sext (nth (dhead d) (dtape d) 0))) ceot 0
                        else setm s1 ceot 1) else s1 in
  let h2 := if rd && ok then S (dhead d) else dhead d in
  let late := dlate d || (rd && negb ok && match drew d with [] => true | _ => false end) in
  (setm (setm (setm s2 cwr 0) crd 0) crw 0,
   mkD (dtape d) (if rw then 0 else h2) (if wr then dout d ++ [memv s rout mod 256] else dout d) late
       (if rw then drew d ++ [h2] else drew d)).

Definition tstep (c : hst * dev) : hst * dev := device (subleq A (fst c)) (snd c).

Fixpoint trun (n : nat) (c : hst * dev) : hst * dev :=
  match n with O => c | S k => trun k (tstep c) end.

(* the twenty instructions of the decoding loop, an instruction A B C at 3k *)
Definition decode_loop : list (nat * nat * nat) :=
  [(t2c, t2c, 3); (t1c, t1c, 6); (neg1c, crd, 9); (rin, t1c, 12); (t1c, t2c, 15); (zc, t2c, 21);
   (zc, zc, 27); (zc, t1c, 60); (zc, zc, 45); (neg1c, crd, 30); (rin, rout, 33); (neg1c, cwr, 36);
   (onec, t2c, 42); (zc, zc, 27); (zc, zc, 0); (neg1c, crd, 48); (rin, rout, 51); (neg1c, cwr, 54);
   (onec, t1c, 42); (zc, zc, 48)].

Definition progP : list (nat * nat * nat) := decode_loop ++ [(zc, zc, haltc)].

Definition progPstar : list (nat * nat * nat) :=
  decode_loop ++ [(neg1c, crw, 63); (neg1c, crd, 66); (ceot, eokc, haltc); (rin, zc, 72); (zc, rout, 75);
                  (neg1c, cwr, 78); (zc, zc, 63)].

Definition word (prog : list (nat * nat * nat)) (j : nat) : nat :=
  let '(a, b, c) := nth (j / 3) prog (0, 0, 0) in
  match j mod 3 with 0 => a | 1 => b | _ => c end.

(* the initial memory: the program, the constants ONE, NEG1 and EOK, and zero elsewhere *)
Definition img0 (prog : list (nat * nat * nat)) (j : nat) : nat :=
  if j <? 3 * length prog then word prog j
  else if Nat.eqb j onec then 1 else if Nat.eqb j neg1c then SW A - 1 else if Nat.eqb j eokc then 1 else 0.

Definition image (prog : list (nat * nat * nat)) : list nat := map (img0 prog) (seq 0 (SW A)).

Definition init (prog : list (nat * nat * nat)) (tau : list nat) : hst * dev :=
  (mkH 0 false (image prog), mkD tau 0 [] false []).

End Dev.