/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/dev_sym.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
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 v (i : nat) (c : N) : lf := LF c (List.repeat 0%N i ++ [4%N]).

Definition ep28 := Rc B ([], TV 0)
  ([(S1, v 0 27); (S1, v 1 27); (S1, LF 7 []); (S1, v 2 25); (S1, v 3 24); (S0, LF 2 [])], T0).

Time Eval vm_compute in until_stuck 100000 ep28.