Changeset 2477 for src/joint


Ignore:
Timestamp:
Nov 20, 2012, 1:41:58 PM (7 years ago)
Author:
tranquil
Message:

status_simulation reformulated
definition of joint_classify split up in subdefinitions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2473 r2477  
    9999qed.
    100100
     101definition joint_classify_seq :
     102  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
     103  λp,st,stmt.
     104  match stmt with
     105  [ CALL f args dest ⇒
     106    match function_of_call ?? (ev_genv p) st f with
     107    [ OK fn ⇒
     108      match description_of_function … fn with
     109      [ Internal _ ⇒ cl_call
     110      | External _ ⇒ cl_other
     111      ]
     112    | Error _ ⇒ cl_other
     113    ]
     114  | _ ⇒ cl_other
     115  ].
     116
     117definition joint_classify_step :
     118  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
     119  λp,st,stmt.
     120  match stmt with
     121  [ step_seq s ⇒ joint_classify_seq p st s
     122  | COND _ _ ⇒ cl_jump
     123  ].
     124
     125definition joint_classify_final :
     126  ∀p : evaluation_params.joint_fin_step p → status_class ≝
     127  λp,stmt.
     128  match stmt with
     129  [ GOTO _ ⇒ cl_other
     130  | RETURN ⇒ cl_return
     131  | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     132  ].
     133
    101134definition joint_classify :
    102135  ∀p : evaluation_params.state_pc p → status_class ≝
     
    104137  match fetch_statement ? p … (ev_genv p) (pc … st) with
    105138  [ OK f_s ⇒
    106     let 〈f, s〉 ≝ f_s in
    107     match s with
    108     [ sequential s _ ⇒
    109       match s with
    110       [ step_seq s ⇒
    111         match s with
    112         [ CALL f' args dest ⇒
    113           match function_of_call ?? (ev_genv p) st f' with
    114           [ OK fn ⇒
    115             match description_of_function … fn with
    116             [ Internal _ ⇒ cl_call
    117             | External _ ⇒ cl_other
    118             ]
    119           | Error _ ⇒ cl_other
    120           ]
    121         | _ ⇒ cl_other
    122         ]
    123       | COND _ _ ⇒ cl_jump
    124       ]
    125     | final s ⇒
    126       match s with
    127       [ GOTO _ ⇒ cl_other
    128       | RETURN ⇒ cl_return
    129       | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
    130       ]
     139    match \snd f_s with
     140    [ sequential s _ ⇒ joint_classify_step p st s
     141    | final s ⇒ joint_classify_final p s
    131142    ]
    132143  | Error _ ⇒ cl_other
     
    142153#p #st
    143154whd in match joint_classify; normalize nodelta
    144 lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
    145 elim (fetch_statement ?????) in ⊢ (???%→%);
     155inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
    146156[ * #f * [| * [ #lbl || #b #f #args ]]
    147157  [ * [| #a #lbl #next ]
     
    150160      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
    151161      | #ext ] #next
    152       [ normalize nodelta
    153         lapply (refl … (function_of_call … (ev_genv p) st f'))
    154         elim (function_of_call ?????) in ⊢ (???%→%);
    155         [ #fn normalize nodelta
    156           lapply (refl … (description_of_function … (ev_genv p) fn))
    157           elim (description_of_function ?? fn) in ⊢ (???%→%); #fd
     162      [ whd in match joint_classify_step; whd in match joint_classify_seq;
     163        normalize nodelta
     164        inversion (function_of_call ?????) normalize nodelta
     165        [ #fn
     166          inversion (description_of_function ?? fn) #fd
    158167          #EQfd
    159168        | #e
     
    166175[|*: #ABS normalize in ABS; destruct(ABS) ]
    167176normalize nodelta #_
    168 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
     177%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
     178%{EQfd} %{EQfn} %
    169179qed.
    170180
Note: See TracChangeset for help on using the changeset viewer.