Changeset 1594 for src/RTLabs/Traces.ma

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:

• src/RTLabs/Traces.ma (modified) (6 diffs)

src/RTLabs/Traces.ma

@@ -410 +410 @@
 (* Don't need to know that labels break loops because we have termination. *)
 
-record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
+record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
   new_state : state;
   termination_count : nat;
   remainder : flat_trace io_out io_in ge new_state;
-  terminates : nth_is_return ge termination_count O new_state remainder;
   cost_labelled : well_cost_labelled_state new_state;
   new_trace : T new_state
 }.
 
-definition replace_new_trace : ∀ge,T1,T2.
-  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
+record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
+  ends : trace_ends_with_ret;
+  trace_res :> trace_result ge (T ends);
+  terminates :
+    (* We handle returns specially *)
+    match ends with
+    [ doesnt_end_with_ret ⇒ nth_is_return ge (termination_count ?? trace_res) O (new_state ?? trace_res) (remainder ?? trace_res)
+    | ends_with_ret ⇒ True
+    ]
+}.
+
+definition replace_sub_trace : ∀ge,T1,T2.
+  ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝
 λge,T1,T2,r,trace.
-  mk_make_result ge T2
+  mk_sub_trace_result ge T2
+    (ends … r)
+    (mk_trace_result ge (T2 (ends … r))
+      (new_state … r)
+      (termination_count … r)
+      (remainder … r)
+      (cost_labelled … r)
+      trace
+    )
+    (terminates … r)
+.
+
+definition replace_trace : ∀ge,T1,T2.
+  ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝
+λge,T1,T2,r,trace.
+  mk_trace_result ge T2
     (new_state … r)
     (termination_count … r)
     (remainder … r)
-    (terminates … r)
     (cost_labelled … r)
-    trace.
+    trace
+.
 
 let rec make_label_return n ge s
@@ -436 +461 @@
   (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
   (TERMINATES: nth_is_return ge n O s trace)
-  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
+  : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝
 
   let r ≝ make_label_label n ge s trace ???? in
-  match new_trace … r with
-  [ dp ends tll ⇒
-    match ends return λx. trace_label_label ? x ?? → ? with
-    [ ends_with_ret ⇒ λtll.
-        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
-    | doesnt_end_with_ret ⇒ λtll.
-        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
-                   (remainder … r) ??? (terminates … r) in
-          replace_new_trace … r'
-            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
-    ] tll
-  ]
+  match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with
+  [ ends_with_ret ⇒ λtll,term.
+      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
+  | doesnt_end_with_ret ⇒ λtll,term.
+      let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
+                 (remainder … r) ??? term in
+        replace_trace … r'
+          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
+  ] (new_trace … r) (terminates … r)
 
 and make_label_label n ge s
@@ -458 +480 @@
   (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
   (TERMINATES: nth_is_return ge n O s trace)
-  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
+  : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
 let r ≝ make_any_label n ge s trace ??? in
-match new_trace … r with
-[ dp ends tr ⇒
-  replace_new_trace ??? r
-    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
-]
+  replace_sub_trace ??? r
+    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
 
 and make_any_label n ge s
@@ -471 +490 @@
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
   (TERMINATES: nth_is_return ge n O s trace)
-  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
-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
+  : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
+match 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
 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
 | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
@@ -479 +498 @@
         match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
         [ true ⇒ λCS.
-            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 ???))
+            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 ???)) ?
         | false ⇒ λCS.
             let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
-            match new_trace … r with
-            [ dp ends trc ⇒
-                replace_new_trace ??? r
-                  (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??))
-            ]
+                replace_sub_trace ??? r
+                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
         ] (refl ??)
     | cl_jump ⇒ λCL.
-        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 ???))
+        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 ???)) ?
     | cl_call ⇒ λCL. ?
-    | cl_return ⇒ λCL. ?
+    | cl_return ⇒ λCL.
+        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)) ?
     ] (refl ? (RTLabs_classify start))
 | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
@@ -507 +524 @@
 | //
 |
-|
-| @(nth_is_return_notfn … TERMINATES) %2 @CL
+| %{tr} @EV
 | @(well_cost_labelled_state_step  … EV) //
+| @I
 | %{tr} @EV
 | % whd in ⊢ (% → ?); >CL #E destruct
 | @(well_cost_labelled_jump … EV) //
+| @(well_cost_labelled_state_step  … EV) //
+| @(nth_is_return_notfn … TERMINATES) %2 @CL
 |
-| @(nth_is_return_notfn … TERMINATES) %1 @CL
-| @(well_cost_labelled_state_step  … EV) //
 | %{tr} @EV
 | % whd in ⊢ (% → ?); >CL #E destruct
 | @CS
+| @(well_cost_labelled_state_step  … EV) //
+| @(nth_is_return_notfn … TERMINATES) %1 @CL
+| % whd in ⊢ (% → ?); >CS #E destruct
+| @CL
 | %{tr} @EV
-| @CL
-| % whd in ⊢ (% → ?); >CS #E destruct
-| @(well_cost_labelled_state_step … EV) //
+| @(well_cost_labelled_state_step  … EV) //
 | @(nth_is_return_notfn … TERMINATES) %1 @CL
 | inversion TERMINATES