source: src/RTLabs/debug.ma @ 1324

Last change on this file since 1324 was 797, checked in by campbell, 10 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
RevLine 
[775]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
[797]9| Fail : errmsg → ministate
[775]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]
[797]26                   | e_interact o k ⇒ [Fail (msg StoppedMidIO)]
27                   | e_wrong m ⇒ [Fail m]
[775]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)
[797]36                                       | Error m ⇒ [Fail m]
[775]37                                       ]
38                         ]
[797]39                     | e_wrong m ⇒ [Fail m]
[775]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.