- Timestamp:
- Nov 20, 2012, 1:41:58 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Traces.ma
r2473 r2477 99 99 qed. 100 100 101 definition 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 117 definition 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 125 definition 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 101 134 definition joint_classify : 102 135 ∀p : evaluation_params.state_pc p → status_class ≝ … … 104 137 match fetch_statement ? p … (ev_genv p) (pc … st) with 105 138 [ 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 131 142 ] 132 143 | Error _ ⇒ cl_other … … 142 153 #p #st 143 154 whd in match joint_classify; normalize nodelta 144 lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st))) 145 elim (fetch_statement ?????) in ⊢ (???%→%); 155 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta 146 156 [ * #f * [| * [ #lbl || #b #f #args ]] 147 157 [ * [| #a #lbl #next ] … … 150 160 | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg 151 161 | #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 158 167 #EQfd 159 168 | #e … … 166 175 [|*: #ABS normalize in ABS; destruct(ABS) ] 167 176 normalize nodelta #_ 168 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/ 177 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} 178 %{EQfd} %{EQfn} % 169 179 qed. 170 180
Note: See TracChangeset
for help on using the changeset viewer.