File size: 3,872 Bytes
5ee1fb5 a9ea017 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 | (* 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.
|