source: src/RTLabs/debug.ma @ 3096

Last change on this file since 3096 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 1.8 KB
Line 
1include "common/Animation.ma".
2include "RTLabs/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.