Changeset 1594


Ignore:
Timestamp:
Dec 7, 2011, 4:24:35 PM (8 years ago)
Author:
campbell
Message:

Rework handling of termination information in RTLabs structured traces to
avoid requiring it when we don't have it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1586 r1594  
    410410(* Don't need to know that labels break loops because we have termination. *)
    411411
    412 record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
     412record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
    413413  new_state : state;
    414414  termination_count : nat;
    415415  remainder : flat_trace io_out io_in ge new_state;
    416   terminates : nth_is_return ge termination_count O new_state remainder;
    417416  cost_labelled : well_cost_labelled_state new_state;
    418417  new_trace : T new_state
    419418}.
    420419
    421 definition replace_new_trace : ∀ge,T1,T2.
    422   ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
     420record 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
     431definition replace_sub_trace : ∀ge,T1,T2.
     432  ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝
    423433λ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
     446definition 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
    425450    (new_state … r)
    426451    (termination_count … r)
    427452    (remainder … r)
    428     (terminates … r)
    429453    (cost_labelled … r)
    430     trace.
     454    trace
     455.
    431456
    432457let rec make_label_return n ge s
     
    436461  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    437462  (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) ≝
    439464
    440465  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)
    453475
    454476and make_label_label n ge s
     
    458480  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    459481  (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) ≝
    461483let 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)
    467486
    468487and make_any_label n ge s
     
    471490  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    472491  (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') with
     492  : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
     493match 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
    475494[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
    476495| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
     
    479498        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    480499        [ 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 ???)) ?
    482501        | false ⇒ λCS.
    483502            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) ??)
    489505        ] (refl ??)
    490506    | 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 ???)) ?
    492508    | 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)) ?
    494511    ] (refl ? (RTLabs_classify start))
    495512| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
     
    507524| //
    508525|
    509 |
    510 | @(nth_is_return_notfn … TERMINATES) %2 @CL
     526| %{tr} @EV
    511527| @(well_cost_labelled_state_step  … EV) //
     528| @I
    512529| %{tr} @EV
    513530| % whd in ⊢ (% → ?); >CL #E destruct
    514531| @(well_cost_labelled_jump … EV) //
     532| @(well_cost_labelled_state_step  … EV) //
     533| @(nth_is_return_notfn … TERMINATES) %2 @CL
    515534|
    516 | @(nth_is_return_notfn … TERMINATES) %1 @CL
    517 | @(well_cost_labelled_state_step  … EV) //
    518535| %{tr} @EV
    519536| % whd in ⊢ (% → ?); >CL #E destruct
    520537| @CS
     538| @(well_cost_labelled_state_step  … EV) //
     539| @(nth_is_return_notfn … TERMINATES) %1 @CL
     540| % whd in ⊢ (% → ?); >CS #E destruct
     541| @CL
    521542| %{tr} @EV
    522 | @CL
    523 | % whd in ⊢ (% → ?); >CS #E destruct
    524 | @(well_cost_labelled_state_step … EV) //
     543| @(well_cost_labelled_state_step  … EV) //
    525544| @(nth_is_return_notfn … TERMINATES) %1 @CL
    526545| inversion TERMINATES
Note: See TracChangeset for help on using the changeset viewer.