source: src/RTLabs/debug.ma @ 775

Last change on this file since 775 was 775, checked in by campbell, 9 years ago

A few useful definitions for when RTLabs programs fail.

File size: 1.7 KB
Line 
1include "common/Animation.ma".
2include "RTLabs/semantics.ma".
3
4inductive ministate : Type[0] ≝
5| Stmt : statement → ministate
6| Call : ministate
7| Ret : ministate
8| NoInput : ministate
9| Fail : ministate
10| MissingStmt : ministate
11| Done : int → ministate
12.
13
14definition mk_ministate : state → ministate ≝
15λs.
16match s with
17[ State f fs m ⇒ match lookup ?? (f_graph (func f)) (next f) with [ Some s ⇒ Stmt s | None ⇒ MissingStmt ]
18| Callstate fd _ _ _ _ ⇒ Call
19| Returnstate _ _ _ _ ⇒ Ret
20].
21
22let rec debug_up_to_aux (n:nat) (input:list eventval) (e:execution ? io_out io_in) : list ministate ≝
23match n with
24[ O ⇒ match e with [ e_step tr s _ ⇒ [mk_ministate s]
25                   | e_stop tr r m ⇒ [Done r]
26                   | _ ⇒ [Fail]
27                   ]
28| S m ⇒ match e with [ e_step tr s e' ⇒ (mk_ministate s)::(debug_up_to_aux m input e')
29                     | e_stop tr r m ⇒ [Done r]
30                     | e_interact o k ⇒
31                         match input with
32                         [ nil ⇒ [NoInput]
33                         | cons h tl ⇒ match get_input o h with
34                                       [ OK i ⇒ debug_up_to_aux m tl (k i)
35                                       | _ ⇒ [Fail]
36                                       ]
37                         ]
38                     | e_wrong ⇒ [Fail]
39                     ]
40].
41
42let rec number_list (A:Type[0]) (l:list A) (n:nat) on l : list (nat × A) ≝
43match l with
44[ nil ⇒ nil ?
45| cons h t ⇒ 〈n,h〉::(number_list A t (S n))
46].
47
48definition debug_up_to : RTLabs_program → nat → list eventval → list (nat × ministate) ≝
49λp,n,i. number_list ? (debug_up_to_aux n i (exec_inf ?? RTLabs_fullexec p)) 0.
50
Note: See TracBrowser for help on using the repository browser.