Changeset 2477 for src/joint

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:

• src/joint/Traces.ma (modified) (5 diffs)

src/joint/Traces.ma

@@ -99 +99 @@
 qed.
 
+definition joint_classify_seq :
+  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
+  λp,st,stmt.
+  match stmt with
+  [ CALL f args dest ⇒
+    match function_of_call ?? (ev_genv p) st f with
+    [ OK fn ⇒
+      match description_of_function … fn with
+      [ Internal _ ⇒ cl_call
+      | External _ ⇒ cl_other
+      ]
+    | Error _ ⇒ cl_other
+    ]
+  | _ ⇒ cl_other
+  ].
+
+definition joint_classify_step :
+  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
+  λp,st,stmt.
+  match stmt with
+  [ step_seq s ⇒ joint_classify_seq p st s
+  | COND _ _ ⇒ cl_jump
+  ].
+
+definition joint_classify_final :
+  ∀p : evaluation_params.joint_fin_step p → status_class ≝
+  λp,stmt.
+  match stmt with
+  [ GOTO _ ⇒ cl_other
+  | RETURN ⇒ cl_return
+  | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
+  ].
+
 definition joint_classify :
   ∀p : evaluation_params.state_pc p → status_class ≝
@@ -104 +137 @@
   match fetch_statement ? p … (ev_genv p) (pc … st) with
   [ OK f_s ⇒
-    let 〈f, s〉 ≝ f_s in
-    match s with
-    [ sequential s _ ⇒
-      match s with
-      [ step_seq s ⇒
-        match s with
-        [ CALL f' args dest ⇒
-          match function_of_call ?? (ev_genv p) st f' with
-          [ OK fn ⇒
-            match description_of_function … fn with
-            [ Internal _ ⇒ cl_call
-            | External _ ⇒ cl_other
-            ]
-          | Error _ ⇒ cl_other
-          ]
-        | _ ⇒ cl_other
-        ]
-      | COND _ _ ⇒ cl_jump
-      ]
-    | final s ⇒
-      match s with
-      [ GOTO _ ⇒ cl_other
-      | RETURN ⇒ cl_return
-      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
-      ]
+    match \snd f_s with
+    [ sequential s _ ⇒ joint_classify_step p st s
+    | final s ⇒ joint_classify_final p s
     ]
   | Error _ ⇒ cl_other
@@ -142 +153 @@
 #p #st
 whd in match joint_classify; normalize nodelta
-lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
-elim (fetch_statement ?????) in ⊢ (???%→%);
+inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
 [ * #f * [| * [ #lbl || #b #f #args ]]
   [ * [| #a #lbl #next ]
@@ -150 +160 @@
       | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
       | #ext ] #next
-      [ normalize nodelta
-        lapply (refl … (function_of_call … (ev_genv p) st f'))
-        elim (function_of_call ?????) in ⊢ (???%→%);
-        [ #fn normalize nodelta
-          lapply (refl … (description_of_function … (ev_genv p) fn))
-          elim (description_of_function ?? fn) in ⊢ (???%→%); #fd
+      [ whd in match joint_classify_step; whd in match joint_classify_seq;
+        normalize nodelta
+        inversion (function_of_call ?????) normalize nodelta
+        [ #fn
+          inversion (description_of_function ?? fn) #fd
           #EQfd
         | #e
@@ -166 +175 @@
 [|*: #ABS normalize in ABS; destruct(ABS) ]
 normalize nodelta #_
-%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
+%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
+%{EQfd} %{EQfn} % 
 qed.