Changeset 1654


Ignore:
Timestamp:
Jan 23, 2012, 5:37:26 PM (6 years ago)
Author:
campbell
Message:

Corrections to structured trace definitions (see the mailing list).
Also update RTLabs work to match.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1653 r1654  
    597597    | cl_call ⇒ λCL.
    598598        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    599         let r' ≝ make_any_label ge depth
    600                    (new_state … r) (remainder … r) ENV_COSTLABELLED ?
    601                    (pi1 … (terminates … r)) TIME ? in
    602         replace_sub_trace … r'
    603           (tal_step_call (RTLabs_status ge) (ends … r')
    604             start next (new_state … r) (new_state … r') ? CL ?
    605             (new_trace … r) (new_trace … r'))
     599        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     600        (* We're about to run into a label, use base case for call *)
     601        [ true ⇒ λCS.
     602            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
     603            doesnt_end_with_ret
     604            (replace_trace … r
     605              (tal_base_call (RTLabs_status ge) start next (new_state … r)
     606                ? CL ? (new_trace … r) CS))
     607        (* otherwise use step case *)
     608        | false ⇒ λCS.
     609            let r' ≝ make_any_label ge depth
     610                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
     611                       (pi1 … (terminates … r)) TIME ? in
     612            replace_sub_trace … r'
     613              (tal_step_call (RTLabs_status ge) (ends … r')
     614                start next (new_state … r) (new_state … r') ? CL ?
     615                (new_trace … r) ? (new_trace … r'))
     616        ] (refl ??)
    606617
    607618    | cl_return ⇒ λCL.
     
    644655| whd @(will_return_notfn … TERMINATES) %2 @CL
    645656| %{tr} @EV
    646 | % whd in ⊢ (% → ?); >CL #E destruct
     657| %1 whd @CL
    647658| @(well_cost_labelled_jump … EV) //
    648659| @(well_cost_labelled_state_step  … EV) //
     660| %{tr} @EV
     661| (* TODO oh dear *)
     662| cases (will_return_call … TERMINATES) #H @le_S_to_le
    649663| cases r #H1 #H2 #H3 #H4 * #H5
    650664  cases (will_return_call … CL TERMINATES)
    651665  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
     666| whd in ⊢ (?%); >CS % #E destruct
    652667| (* TODO oh dear *)
    653668| %{tr} @EV
     
    671686| whd @(will_return_notfn … TERMINATES) %1 @CL
    672687| %{tr} @EV
    673 | % whd in ⊢ (% → ?); >CL #E destruct
     688| %2 whd @CL
    674689| @CS
    675690| @(well_cost_labelled_state_step  … EV) //
     
    782797% whd in ⊢ (% → ?); >NOT_COST #E destruct
    783798qed.
    784 
     799(* I'll come back to this.
    785800definition fp_add_terminating_call : ∀ge,s,s1,s'.
    786801  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
     
    799814    rem
    800815].
    801 
     816*)
    802817(*
    803818let corec make_label_diverges ge s
  • src/common/StructuredTraces.ma

    r1652 r1654  
    4343          trace_label_label S ends_flag start_status end_status
    4444with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
     45  (* Single steps within a function which reach a label.
     46     Note that this is the only case applicable for a jump. *)
    4547  | tal_base_not_return:
    4648      ∀start_status: S.
    4749      ∀final_status: S.
    4850        as_execute S start_status final_status →
    49         ¬ as_classifier S start_status cl_return →
     51        (as_classifier S start_status cl_jump ∨
     52         as_classifier S start_status cl_other) →
    5053        as_costed S final_status →
    5154          trace_any_label S doesnt_end_with_ret start_status final_status
     
    5659        as_classifier S start_status cl_return →
    5760          trace_any_label S ends_with_ret start_status final_status
     61  (* A call followed by a label on return. *)
     62  | tal_base_call:
     63      ∀status_pre_fun_call: S.
     64      ∀status_start_fun_call: S.
     65      ∀status_final: S.
     66        as_execute S status_pre_fun_call status_start_fun_call →
     67        ∀H:as_classifier S status_pre_fun_call cl_call.
     68          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
     69          trace_label_return S status_start_fun_call status_final →
     70          as_costed S status_final →
     71            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
     72  (* A call followed by a non-empty trace. *)
    5873  | tal_step_call:
    5974      ∀end_flag: trace_ends_with_ret.
     
    6681          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    6782          trace_label_return S status_start_fun_call status_after_fun_call →
     83          ¬ as_costed S status_after_fun_call →
    6884          trace_any_label S end_flag status_after_fun_call status_final →
    6985            trace_any_label S end_flag status_pre_fun_call status_final
     
    120136          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    121137          trace_label_return S status_start_fun_call status_after_fun_call →
     138          ¬ as_costed S status_after_fun_call →
    122139          trace_any_call S status_after_fun_call status_final →
    123140            trace_any_call S status_pre_fun_call status_final
     
    137154[ tal_base_not_return start final _ _ C ⇒ C
    138155| tal_base_return _ _  _ _ ⇒ I
    139 | tal_step_call f pre start after final X C RET LR tr' ⇒ trace_any_label_label … tr'
     156| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     157| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    140158| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    141159].
Note: See TracChangeset for help on using the changeset viewer.