Changeset 1653


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

Start on building finite sections of non-terminating structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1651 r1653  
    751751qed.
    752752
     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
     757inductive 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
     768definition 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.
     775match 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
     783qed.
     784
     785definition 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.
     793match 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
    753802(*
    754803let corec make_label_diverges ge s
Note: See TracChangeset for help on using the changeset viewer.