Changeset 1670

Timestamp:

Feb 1, 2012, 4:16:04 PM (7 years ago)

Author:

campbell

Message:

Snapshot of non-terminating RTLabs structured traces work.

File:

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

src/RTLabs/Traces.ma

@@ -54 +54 @@
   normalize try #a try #b try #c try #d try #e try #g try #h destruct
 ] qed.
+
+lemma RTLabs_not_cost : ∀ge,s.
+  RTLabs_cost s = false →
+  ¬ as_costed (RTLabs_status ge) s.
+#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
+qed.
 
 (* Before attempting to construct a structured trace, let's show that we can
@@ -580 +586 @@
               doesnt_end_with_ret
               (mk_trace_result ge ??? next trace' ?
-                (tal_base_not_return (RTLabs_status ge) start next ???) ?)
+                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ?)
         (* An ordinary step, keep going. *)
         | false ⇒ λCS.
@@ -586 +592 @@
                 replace_sub_trace … r
                   (tal_step_default (RTLabs_status ge) (ends … r)
-                     start next (new_state … r) ? (new_trace … r) ??)
+                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS))
         ] (refl ??)
         
@@ -613 +619 @@
               (tal_step_call (RTLabs_status ge) (ends … r')
                 start next (new_state … r) (new_state … r') ? CL ?
-                (new_trace … r) ? (new_trace … r'))
+                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r'))
         ] (refl ??)
 
@@ -664 +670 @@
   cases (will_return_call … CL TERMINATES)
   #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
-| whd in ⊢ (?%); >CS % #E destruct
 | (* TODO oh dear *)
 | %{tr} @EV
@@ -687 +692 @@
 | %{tr} @EV
 | %2 whd @CL
-| @CS
 | @(well_cost_labelled_state_step  … EV) //
 | cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
-| % whd in ⊢ (% → ?); >CS #E destruct
 | @CL
 | %{tr} @EV
@@ -770 +773 @@
    use the fact that the trace is soundly labelled to achieve this. *)
 
-inductive finite_prefix (ge:genv) : state → Type[0] ≝
+inductive finite_prefix (ge:genv) : state → Prop ≝
 | fp_tal : ∀s,s'.
            trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
@@ -790 +793 @@
 match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
 [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf 
-    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER ?)
+    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
     rem
 | fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf 
-    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER ?) rem
+    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
 ].
-% whd in ⊢ (% → ?); >NOT_COST #E destruct
-qed.
-(* I'll come back to this.
+
 definition fp_add_terminating_call : ∀ge,s,s1,s'.
   (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
@@ -804 +805 @@
   trace_label_return (RTLabs_status ge) s1 s' →
   as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
+  RTLabs_cost s' = false →
   finite_prefix ge s ≝
 λge,s,s1,s',EVAL,CALL,fp.
-match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → finite_prefix ge s with
-[ fp_tal s' sf TAL rem ⇒ λTLR,RET. fp_tal ge s sf
-    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR TAL)
+match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with
+[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
+    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
     rem
-| fp_tac s' sf TAC rem ⇒ λTLR,RET. fp_tac ge s sf
-    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR TAC)
+| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
+    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
     rem
 ].
-*)
+
+definition termination_oracle ≝ ∀ge,depth,s,trace.
+  inhabited (will_return ge depth s trace) ⊎ ¬ inhabited (will_return ge depth s trace).
+
+let rec finite_segment ge s n trace
+  (ORACLE: termination_oracle)
+  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
+  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
+  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
+  (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true))
+  : finite_prefix ge s ≝
+match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
+[ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
+| S n' ⇒ 
+    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
+    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
+    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
+        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
+        [ cl_other ⇒ λCL.
+            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
+            [ true ⇒ λCS.
+                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
+            | false ⇒ λCS.
+                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in
+                fp_add_default ge ?? CL fs ? CS
+            ] (refl ??)
+        | cl_jump ⇒ λCL.
+            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
+        | cl_call ⇒ λCL.
+            match ORACLE ge O next trace' with
+            [ inl TERMINATES ⇒
+                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ??? in
+                ?
+            | inr NO_TERMINATION ⇒ ?
+            ]
+        | cl_return ⇒ λCL. ⊥
+        ] (refl ??)
+    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
+    ]
+] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT.
+[ 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
+| 3: @(absurd ?? NO_TERMINATION)
+     %{0} % @wr_base //
+| 4: @(well_cost_labelled_jump … EV) //
+| 5,6: /2/
+| 8: @(well_cost_labelled_state_step … EV) //
+| 9: @(well_cost_labelled_call … EV) //
+| 10: cases TERMINATES //
+| 12,13,14: /2/
+| 15: @(well_cost_labelled_state_step … EV) //
+| 16: @(not_to_not … NO_TERMINATION)
+     * #depth * #TERM %{depth} % @wr_step /2/
+] cases daemon qed.
+
 (*
 let corec make_label_diverges ge s