source: src/RTLabs/debug.ma @ 1782

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 1.8 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 : errmsg → 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                   | e_interact o k ⇒ [Fail (msg StoppedMidIO)]
27                   | e_wrong m ⇒ [Fail m]
28                   ]
29| S m ⇒ match e with [ e_step tr s e' ⇒ (mk_ministate s)::(debug_up_to_aux m input e')
30                     | e_stop tr r m ⇒ [Done r]
31                     | e_interact o k ⇒
32                         match input with
33                         [ nil ⇒ [NoInput]
34                         | cons h tl ⇒ match get_input o h with
35                                       [ OK i ⇒ debug_up_to_aux m tl (k i)
36                                       | Error m ⇒ [Fail m]
37                                       ]
38                         ]
39                     | e_wrong m ⇒ [Fail m]
40                     ]
41].
42
43let rec number_list (A:Type[0]) (l:list A) (n:nat) on l : list (nat × A) ≝
44match l with
45[ nil ⇒ nil ?
46| cons h t ⇒ 〈n,h〉::(number_list A t (S n))
47].
48
49definition debug_up_to : RTLabs_program → nat → list eventval → list (nat × ministate) ≝
50λp,n,i. number_list ? (debug_up_to_aux n i (exec_inf ?? RTLabs_fullexec p)) 0.
51
Note: See TracBrowser for help on using the repository browser.