Changeset 1594 for src/RTLabs/Traces.ma
- Timestamp:
- Dec 7, 2011, 4:24:35 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1586 r1594 410 410 (* Don't need to know that labels break loops because we have termination. *) 411 411 412 record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {412 record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ { 413 413 new_state : state; 414 414 termination_count : nat; 415 415 remainder : flat_trace io_out io_in ge new_state; 416 terminates : nth_is_return ge termination_count O new_state remainder;417 416 cost_labelled : well_cost_labelled_state new_state; 418 417 new_trace : T new_state 419 418 }. 420 419 421 definition replace_new_trace : ∀ge,T1,T2. 422 ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝ 420 record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ { 421 ends : trace_ends_with_ret; 422 trace_res :> trace_result ge (T ends); 423 terminates : 424 (* We handle returns specially *) 425 match ends with 426 [ doesnt_end_with_ret ⇒ nth_is_return ge (termination_count ?? trace_res) O (new_state ?? trace_res) (remainder ?? trace_res) 427 | ends_with_ret ⇒ True 428 ] 429 }. 430 431 definition replace_sub_trace : ∀ge,T1,T2. 432 ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝ 423 433 λge,T1,T2,r,trace. 424 mk_make_result ge T2 434 mk_sub_trace_result ge T2 435 (ends … r) 436 (mk_trace_result ge (T2 (ends … r)) 437 (new_state … r) 438 (termination_count … r) 439 (remainder … r) 440 (cost_labelled … r) 441 trace 442 ) 443 (terminates … r) 444 . 445 446 definition replace_trace : ∀ge,T1,T2. 447 ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝ 448 λge,T1,T2,r,trace. 449 mk_trace_result ge T2 425 450 (new_state … r) 426 451 (termination_count … r) 427 452 (remainder … r) 428 (terminates … r)429 453 (cost_labelled … r) 430 trace. 454 trace 455 . 431 456 432 457 let rec make_label_return n ge s … … 436 461 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 437 462 (TERMINATES: nth_is_return ge n O s trace) 438 : make_result ge (trace_label_return (RTLabs_status ge) s) ≝463 : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝ 439 464 440 465 let r ≝ make_label_label n ge s trace ???? in 441 match new_trace … r with 442 [ dp ends tll ⇒ 443 match ends return λx. trace_label_label ? x ?? → ? with 444 [ ends_with_ret ⇒ λtll. 445 replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll) 446 | doesnt_end_with_ret ⇒ λtll. 447 let r' ≝ make_label_return (termination_count … r) ge (new_state … r) 448 (remainder … r) ??? (terminates … r) in 449 replace_new_trace … r' 450 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r')) 451 ] tll 452 ] 466 match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with 467 [ ends_with_ret ⇒ λtll,term. 468 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll) 469 | doesnt_end_with_ret ⇒ λtll,term. 470 let r' ≝ make_label_return (termination_count … r) ge (new_state … r) 471 (remainder … r) ??? term in 472 replace_trace … r' 473 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r')) 474 ] (new_trace … r) (terminates … r) 453 475 454 476 and make_label_label n ge s … … 458 480 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 459 481 (TERMINATES: nth_is_return ge n O s trace) 460 : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝482 : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝ 461 483 let r ≝ make_any_label n ge s trace ??? in 462 match new_trace … r with 463 [ dp ends tr ⇒ 464 replace_new_trace ??? r 465 (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL)) 466 ] 484 replace_sub_trace ??? r 485 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 467 486 468 487 and make_any_label n ge s … … 471 490 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 472 491 (TERMINATES: nth_is_return ge n O s trace) 473 : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝474 match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with492 : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝ 493 match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with 475 494 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 476 495 | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. … … 479 498 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 480 499 [ true ⇒ λCS. 481 mk_ make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???))500 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 482 501 | false ⇒ λCS. 483 502 let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in 484 match new_trace … r with 485 [ dp ends trc ⇒ 486 replace_new_trace ??? r 487 (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??)) 488 ] 503 replace_sub_trace ??? r 504 (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) 489 505 ] (refl ??) 490 506 | cl_jump ⇒ λCL. 491 mk_ make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???))507 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 492 508 | cl_call ⇒ λCL. ? 493 | cl_return ⇒ λCL. ? 509 | cl_return ⇒ λCL. 510 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ? 494 511 ] (refl ? (RTLabs_classify start)) 495 512 | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ … … 507 524 | // 508 525 | 509 | 510 | @(nth_is_return_notfn … TERMINATES) %2 @CL 526 | %{tr} @EV 511 527 | @(well_cost_labelled_state_step … EV) // 528 | @I 512 529 | %{tr} @EV 513 530 | % whd in ⊢ (% → ?); >CL #E destruct 514 531 | @(well_cost_labelled_jump … EV) // 532 | @(well_cost_labelled_state_step … EV) // 533 | @(nth_is_return_notfn … TERMINATES) %2 @CL 515 534 | 516 | @(nth_is_return_notfn … TERMINATES) %1 @CL517 | @(well_cost_labelled_state_step … EV) //518 535 | %{tr} @EV 519 536 | % whd in ⊢ (% → ?); >CL #E destruct 520 537 | @CS 538 | @(well_cost_labelled_state_step … EV) // 539 | @(nth_is_return_notfn … TERMINATES) %1 @CL 540 | % whd in ⊢ (% → ?); >CS #E destruct 541 | @CL 521 542 | %{tr} @EV 522 | @CL 523 | % whd in ⊢ (% → ?); >CS #E destruct 524 | @(well_cost_labelled_state_step … EV) // 543 | @(well_cost_labelled_state_step … EV) // 525 544 | @(nth_is_return_notfn … TERMINATES) %1 @CL 526 545 | inversion TERMINATES
Note: See TracChangeset
for help on using the changeset viewer.