Changeset 1654 for src/RTLabs/Traces.ma


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

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

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.