Changeset 1653
 Timestamp:
 Jan 23, 2012, 5:37:25 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1651 r1653 751 751 qed. 752 752 753 (* When constructing an infinite trace, we need to be able to grab the finite 754 portion of the trace for the next [trace_label_diverges] constructor. We 755 use the fact that the trace is soundly labelled to achieve this. *) 756 757 inductive finite_prefix (ge:genv) : state → Type[0] ≝ 758  fp_tal : ∀s,s'. 759 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → 760 flat_trace io_out io_in ge s' → 761 finite_prefix ge s 762  fp_tac : ∀s,s'. 763 trace_any_call (RTLabs_status ge) s s' → 764 flat_trace io_out io_in ge s' → 765 finite_prefix ge s 766 . 767 768 definition fp_add_default : ∀ge,s,s'. 769 RTLabs_classify s = cl_other → 770 finite_prefix ge s' → 771 (∃t. eval_statement ge s = Value ??? 〈t,s'〉) → 772 RTLabs_cost s' = false → 773 finite_prefix ge s ≝ 774 λge,s,s',OTHER,fp. 775 match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with 776 [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf 777 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER ?) 778 rem 779  fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf 780 (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER ?) rem 781 ]. 782 % whd in ⊢ (% → ?); >NOT_COST #E destruct 783 qed. 784 785 definition fp_add_terminating_call : ∀ge,s,s1,s'. 786 (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → 787 ∀CALL:RTLabs_classify s = cl_call. 788 finite_prefix ge s' → 789 trace_label_return (RTLabs_status ge) s1 s' → 790 as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' → 791 finite_prefix ge s ≝ 792 λge,s,s1,s',EVAL,CALL,fp. 793 match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → finite_prefix ge s with 794 [ fp_tal s' sf TAL rem ⇒ λTLR,RET. fp_tal ge s sf 795 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR TAL) 796 rem 797  fp_tac s' sf TAC rem ⇒ λTLR,RET. fp_tac ge s sf 798 (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR TAC) 799 rem 800 ]. 801 753 802 (* 754 803 let corec make_label_diverges ge s
Note: See TracChangeset
for help on using the changeset viewer.