source: src/RTLabs/Traces.ma @ 1537

Last change on this file since 1537 was 1537, checked in by campbell, 8 years ago

A preliminary definition of the abstract status record for RTLabs.

File size: 1.3 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5definition RTLabs_classify ≝
6    (λs. match s with
7         [ State f fs m ⇒
8             match lookup_present ?? (f_graph (func f)) (next f) ? with
9             [ St_cost _ _ ⇒ cl_cost
10             | _ ⇒ cl_nocost
11             ]
12         | Callstate _ _ _ _ _ ⇒ cl_call
13         | Returnstate _ _ _ _ ⇒ cl_return
14         ]).
15@(next_ok f)
16qed.
17
18definition RTLabs_status : genv → abstract_status ≝
19λge.
20  mk_abstract_status
21    state
22    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
23    (λs,c. RTLabs_classify s = c)
24    (λs,s'. match s with
25      [ dp s p ⇒
26        match s return λs. RTLabs_classify s = cl_call → ? with
27        [ Callstate fd args dst stk m ⇒
28          λ_. match s' with
29          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
30          | _ ⇒ False
31          ]
32        | State f fs m ⇒ λH.⊥
33        | _ ⇒ λH.⊥
34        ] p
35      ]).
36[ normalize in H; destruct
37| cases f * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15
38  whd in H:(??%?); cases (lookup_present LabelTag statement (f_graph (func f)) (next f) ?) in H;
39  normalize try #a try #b try #c try #d try #e try #g try #h
40  destruct
41] qed.
Note: See TracBrowser for help on using the repository browser.