include "common/Animation.ma".
include "RTLabs/RTLabs_semantics.ma".

inductive ministate : Type[0] ≝
| Stmt : statement → ministate
| Call : ministate
| Ret : ministate
| NoInput : ministate
| Fail : errmsg → ministate
| MissingStmt : ministate
| Done : int → ministate
.

definition mk_ministate : state → ministate ≝
λs.
match s with
[ State f fs m ⇒ match lookup ?? (f_graph (func f)) (next f) with [ Some s ⇒ Stmt s | None ⇒ MissingStmt ]
| Callstate fd _ _ _ _ ⇒ Call
| Returnstate _ _ _ _ ⇒ Ret
].

let rec debug_up_to_aux (n:nat) (input:list eventval) (e:execution ? io_out io_in) : list ministate ≝
match n with
[ O ⇒ match e with [ e_step tr s _ ⇒ [mk_ministate s]
                   | e_stop tr r m ⇒ [Done r]
                   | e_interact o k ⇒ [Fail (msg StoppedMidIO)]
                   | e_wrong m ⇒ [Fail m]
                   ]
| S m ⇒ match e with [ e_step tr s e' ⇒ (mk_ministate s)::(debug_up_to_aux m input e')
                     | e_stop tr r m ⇒ [Done r]
                     | e_interact o k ⇒ 
                         match input with
                         [ nil ⇒ [NoInput]
                         | cons h tl ⇒ match get_input o h with
                                       [ OK i ⇒ debug_up_to_aux m tl (k i)
                                       | Error m ⇒ [Fail m]
                                       ]
                         ]
                     | e_wrong m ⇒ [Fail m]
                     ]
].

let rec number_list (A:Type[0]) (l:list A) (n:nat) on l : list (nat × A) ≝
match l with
[ nil ⇒ nil ?
| cons h t ⇒ 〈n,h〉::(number_list A t (S n))
].

definition debug_up_to : RTLabs_program → nat → list eventval → list (nat × ministate) ≝
λp,n,i. number_list ? (debug_up_to_aux n i (exec_inf ?? RTLabs_fullexec p)) 0.