Changeset 1654 for src/RTLabs
 Timestamp:
 Jan 23, 2012, 5:37:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1653 r1654 597 597  cl_call ⇒ λCL. 598 598 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 ??) 606 617 607 618  cl_return ⇒ λCL. … … 644 655  whd @(will_return_notfn … TERMINATES) %2 @CL 645 656  %{tr} @EV 646  % whd in ⊢ (% → ?); >CL #E destruct657  %1 whd @CL 647 658  @(well_cost_labelled_jump … EV) // 648 659  @(well_cost_labelled_state_step … EV) // 660  %{tr} @EV 661  (* TODO oh dear *) 662  cases (will_return_call … TERMINATES) #H @le_S_to_le 649 663  cases r #H1 #H2 #H3 #H4 * #H5 650 664 cases (will_return_call … CL TERMINATES) 651 665 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 666  whd in ⊢ (?%); >CS % #E destruct 652 667  (* TODO oh dear *) 653 668  %{tr} @EV … … 671 686  whd @(will_return_notfn … TERMINATES) %1 @CL 672 687  %{tr} @EV 673  % whd in ⊢ (% → ?); >CL #E destruct688  %2 whd @CL 674 689  @CS 675 690  @(well_cost_labelled_state_step … EV) // … … 782 797 % whd in ⊢ (% → ?); >NOT_COST #E destruct 783 798 qed. 784 799 (* I'll come back to this. 785 800 definition fp_add_terminating_call : ∀ge,s,s1,s'. 786 801 (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → … … 799 814 rem 800 815 ]. 801 816 *) 802 817 (* 803 818 let corec make_label_diverges ge s
Note: See TracChangeset
for help on using the changeset viewer.