/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/dev_visit.v · raw
 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
Require Import ssim.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.

Definition ustep (st : N * cfg * bool) : N * cfg * bool :=
  let '(k, c, stop) := st in
  if stop then st else
  match sstep c with Some (c', _) => (N.succ k, c', false) | None => (k, c, true) end.
Definition until_stuck (fuel : positive) (c : cfg) := Pos.iter ustep (0%N, c, false) fuel.
Definition k (n : N) : lf := LF n [].
Definition L28 : list run :=
     [(S0, k 74808); (S1, k 24912); (S0, k 8277); (S0, k 2737); (S0, k 972); (S1, k 36);
      (S0, k 37); (S0, k 37); (S0, k 44); (S1, k 24); (S0, k 13); (S0, k 9);
      (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5); (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5);
      (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 6); (S1, k 4); (S0, k 1);
      (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 2)].
(* record exit -> cut, moving right *)
Time Eval vm_compute in until_stuck 1000 (Rc B (L28, T0) ([(S1, k 3)], TV 1)).
(* first visit *)
Definition V0 := Lc D ((S0, k 3) :: L28, T0) ([], TV 1).
Time Eval vm_compute in until_stuck 100000 V0.
Definition firstn_cfg (n : nat) (c : cfg) := match c with Rc q (l, t) r => Rc q (firstn n l, t) r | Lc q (l, t) r => Lc q (firstn n l, t) r end.
Fixpoint visits (n : nat) (c : cfg) : list cfg :=
  match n with O => [] | S n' =>
    match until_stuck 100000 c with
    | (_, Rc q l r, _) => firstn_cfg 6 (Rc q l r) :: visits n' (Lc D (push_run S0 (k 3) (match l with (_ :: l', t) => (l', t) | x => x end)) r)
    | _ => []
    end end.