Changeset 2439 for src/RTLabs


Ignore:
Timestamp:
Nov 7, 2012, 4:42:02 PM (7 years ago)
Author:
campbell
Message:

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2314 r2439  
    223223] qed.
    224224
     225definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → ident ≝
     226λge,s.
     227  match s with
     228  [ mk_Sig s p ⇒
     229    match s return λs':RTLabs_state ge. RTLabs_classify s' = cl_call → ident with
     230    [ mk_RTLabs_state s' stk mtc0 ⇒
     231      match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
     232      [ Callstate fd _ _ _ _ ⇒
     233        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
     234        [ nil ⇒ λmtc. ⊥
     235        | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
     236        ]
     237      | State f _ _ ⇒ λ_. λH.⊥
     238      | _ ⇒ λ_. λH.⊥
     239      ] mtc0
     240    ] p
     241  ].
     242[ whd in H:(??%?);
     243  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
     244  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     245| 4,5: normalize in H; destruct (H)
     246| cases mtc
     247| cases mtc #FFP #_ >FFP % #E destruct (E)
     248] qed.
     249
    225250
    226251definition RTLabs_status : genv → abstract_status ≝
     
    231256    RTLabs_deqset
    232257    (RTLabs_state_to_pc ge)
    233     (λs,c. RTLabs_classify s = c)
     258    RTLabs_classify
    234259    (RTLabs_pc_to_cost_label ge)
    235260    (RTLabs_after_return ge)
    236   (λs. RTLabs_is_final s ≠ None ?).
     261    (λs. RTLabs_is_final s ≠ None ?)
     262    (RTLabs_call_ident ge).
    237263
    238264(* Allow us to move between the different notions of when a state is cost
     
    17731799     %{0} % @wr_base //
    17741800| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1775 | 5,6,9,10,11: /3/
     1801| %1 @CL
     1802| 6,9,10,11: /3/
    17761803| cases TRACE_OK #H1 #H2 #H3 #H4
    17771804  % [ @(well_cost_labelled_state_step … EV) //
     
    26942721#ge #flX #s1X #s2X *
    26952722[ #s1 #s2 #EX *
    2696   [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  >CL in CL'; #CL' destruct
     2723  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL' destruct
    26972724  | #CL #CS #CL' @eq_true_to_b @memb_hd
    26982725  ]
    2699 | #s1 #s2 #EX #CL whd in CL; #CL' @⊥ >CL in CL'; #CL' destruct
    2700 | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct
    2701 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct
     2726| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL' destruct
     2727| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct
     2728| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct
    27022729| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
    27032730] qed.
     
    27762803  ]
    27772804| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
     2805  change with (RTLabs_classify ? = ?) in CL1;
     2806  change with (RTLabs_classify ? = ?) in CL3;
    27782807  @eq_true_to_b @memb_cons
    27792808  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
     
    28242853  cases AF1
    28252854| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
     2855  change with (RTLabs_classify ? = ?) in CL;
     2856  change with (RTLabs_classify ? = ?) in CL2;
    28262857  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
    28272858  (* Now that we've inverted the first part of the trace, look for the repeat. *)
     
    28322863      cases (tal_return … CL3 tal3)
    28332864      #EX3 * #CL3' * #E1 #E2 destruct
     2865      change with (RTLabs_classify ? = ?) in CL3';
    28342866      whd in IN:(?%); lapply IN @eqb_elim
    28352867      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct
     
    29412973[ @(no_repeats_of_calls … EX AF) [ assumption |
    29422974  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
    2943 | @no_loops_in_tal //
    2944 ] qed.
    2945 
     2975| @no_loops_in_tal // @CL
     2976] qed.
     2977
Note: See TracChangeset for help on using the changeset viewer.