include "basics/types.ma".
include "basics/bool.ma".
include "basics/jmeq.ma".

inductive status_class : Type[0] ≝
| cl_return : status_class
| cl_jump   : status_class
| cl_call   : status_class
| cl_other : status_class.

record abstract_status : Type[1] ≝ {
  as_status :> Type[0];
  as_execute : as_status → as_status → Prop;
  as_classifier : as_status → status_class → Prop;
  as_costed : as_status → Prop;
  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
}.

inductive trace_ends_with_ret: Type[0] ≝
  | ends_with_ret: trace_ends_with_ret
  | doesnt_end_with_ret: trace_ends_with_ret.

inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
  | tlr_base:
      ∀status_before: S.
      ∀status_after: S.
        trace_label_label S ends_with_ret status_before status_after →
        trace_label_return S status_before status_after
  | tlr_step:
      ∀status_initial: S.
      ∀status_labelled: S.
      ∀status_final: S.
        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
        trace_label_return S status_labelled status_final →
          trace_label_return S status_initial status_final
with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
  | tll_base:
      ∀ends_flag: trace_ends_with_ret.
      ∀start_status: S.
      ∀end_status: S.
        trace_any_label S ends_flag start_status end_status →
        as_costed S start_status →
          trace_label_label S ends_flag start_status end_status
with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
  (* Single steps within a function which reach a label.
     Note that this is the only case applicable for a jump. *)
  | tal_base_not_return:
      ∀start_status: S.
      ∀final_status: S.
        as_execute S start_status final_status →
        (as_classifier S start_status cl_jump ∨
         as_classifier S start_status cl_other) →
        as_costed S final_status →
          trace_any_label S doesnt_end_with_ret start_status final_status
  | tal_base_return:
      ∀start_status: S.
      ∀final_status: S.
        as_execute S start_status final_status →
        as_classifier S start_status cl_return →
          trace_any_label S ends_with_ret start_status final_status
  (* A call followed by a label on return. *)
  | tal_base_call:
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
      ∀status_final: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
          trace_label_return S status_start_fun_call status_final →
          as_costed S status_final →
            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
  (* A call followed by a non-empty trace. *)
  | tal_step_call:
      ∀end_flag: trace_ends_with_ret.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
      ∀status_after_fun_call: S.
      ∀status_final: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
          trace_label_return S status_start_fun_call status_after_fun_call →
          ¬ as_costed S status_after_fun_call →
          trace_any_label S end_flag status_after_fun_call status_final →
            trace_any_label S end_flag status_pre_fun_call status_final
  | tal_step_default:
      ∀end_flag: trace_ends_with_ret.
      ∀status_pre: S.
      ∀status_init: S.
      ∀status_end: S.
        as_execute S status_pre status_init →
        trace_any_label S end_flag status_init status_end →
        as_classifier S status_pre cl_other →
        ¬ (as_costed S status_init) →
          trace_any_label S end_flag status_pre status_end.

inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
  | tac_base:
      ∀status: S.
        as_classifier S status cl_call →
          trace_any_call S status status
  | tac_step_call:
      ∀status_pre_fun_call: S.
      ∀status_after_fun_call: S.
      ∀status_final: S.
      ∀status_start_fun_call: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
          trace_label_return S status_start_fun_call status_after_fun_call →
          ¬ as_costed S status_after_fun_call →
          trace_any_call S status_after_fun_call status_final →
            trace_any_call S status_pre_fun_call status_final
  | tac_step_default:
      ∀status_pre: S.
      ∀status_end: S.
      ∀status_init: S.
        as_execute S status_pre status_init →
        trace_any_call S status_init status_end →
        as_classifier S status_pre cl_other →
        ¬ (as_costed S status_init) →
          trace_any_call S status_pre status_end.

              
inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
  | tlc_base:
      ∀start_status: S.
      ∀end_status: S.
        trace_any_call S start_status end_status →
        as_costed S start_status →
        trace_label_call S start_status end_status
.        

coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
  | tld_step:
      ∀status_initial: S.
      ∀status_labelled: S.
          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
          trace_label_diverges S status_labelled →
            trace_label_diverges S status_initial
  | tld_base:
      ∀status_initial: S.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
        trace_label_call S status_initial status_pre_fun_call →
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          trace_label_diverges S status_start_fun_call →
            trace_label_diverges S status_initial.

(* Version in Prop for showing existence. *)
coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
  | tld_step:
      ∀status_initial: S.
      ∀status_labelled: S.
          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
          trace_label_diverges_exists S status_labelled →
            trace_label_diverges_exists S status_initial
  | tld_base:
      ∀status_initial: S.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
        trace_label_call S status_initial status_pre_fun_call →
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          trace_label_diverges_exists S status_start_fun_call →
            trace_label_diverges_exists S status_initial.

let rec trace_any_label_label S s s' f
  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with 
[ tal_base_not_return start final _ _ C ⇒ C
| tal_base_return _ _  _ _ ⇒ I
| tal_base_call _ _ _ _ _ _ _ C ⇒ C
| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
].

lemma trace_label_label_label : ∀S,s,s',f.
  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
#S #s #s' #f #tr
cases tr
#f #start #end #tr' #C @(trace_any_label_label … tr')
qed.

lemma trace_any_call_call : ∀S,s,s'.
  trace_any_call S s s' → as_classifier S s' cl_call.
#S #s #s' #T elim T //
qed.