include "common/StructuredTraces.ma".

definition is_cl_jump : ∀S : abstract_status.S → bool ≝
λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].

definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.

(* finite flat traces, with recursive structure right to left. The list of
   identifiers represents the call stack *)
inductive flat_trace (S : abstract_status) (start : S) : S → Type[0] ≝
| ft_start : flat_trace S start start
| ft_advance :
  ∀st1,st2.flat_trace S start st1 → as_execute S st1 st2 →
  enforce_costedness … st1 st2 → flat_trace S start st2.

let rec ft_length St s1 s2 (ft : flat_trace St s1 s2) on ft : ℕ ≝
match ft with
[ ft_start ⇒ 0
| ft_advance _ _ pre _ _ ⇒ S (ft_length … pre)
].


(*
  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
  flat_trace S start st2 stack
| ft_advance_call :
  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
  ∀prf : as_classifier ? st1 cl_call.
  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
| ft_advance_tailcall :
  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
  ∀prf : as_classifier ? st1 cl_tailcall.
  flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
| ft_advance_ret :
  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
  as_classifier ? st1 cl_return →
  flat_trace S start st2 stack.
*)

lemma pair_elim' :
  ∀A,B,C : Type[0].∀T : A → B → C.∀t : A × B.
  ∀P : (A×B) → C → Prop.
  P 〈\fst t, \snd t〉 (T (\fst t) (\snd t)) →
  P t (let 〈a, b〉 ≝ t in T a b).
#A #B #C #T * // qed.

let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
  (taa : trace_any_any S st2 st3)
on taa : flat_trace S st1 st3 ≝
match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
[ taa_base s ⇒ λacc.acc
| taa_step st1 st2 st3 H G _ tl ⇒
  λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
] ft.
@hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.

lemma ft_extend_extend_taa : ∀S,st1,st2,st3,st4,ft,taa1,taa2.
  ft_extend_taa S st1 st3 st4 (ft_extend_taa … st2 … ft taa1) taa2 =
  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
#S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
/2/
qed.

definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
  λtaaf : trace_any_any_free S st2 st3.
  match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
  [ taaf_base s ⇒ λft.ft
  | taaf_step s1 s2 s3 pre H G ⇒
    λft.ft_advance … (ft_extend_taa … ft pre) H ?
  | taaf_step_jump s1 s2 s3 pre H G K ⇒
    λft.ft_advance … (ft_extend_taa … ft pre) H ?
  ] ft.
@hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.

definition option_to_list : ∀A.option A → list A ≝ λA,x.
  match x with
  [ Some x ⇒ [x]
  | None ⇒ [ ]
  ].

(*
let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
match ft with
[ ft_start ⇒ [ ]
| ft_advance st1_mid st1' pre1 _ _ ⇒
  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
  [ cl_call ⇒ λprf.
    let id ≝ as_call_ident ? «st1_mid, prf» in
    id :: ft_stack … pre1
  | cl_tailcall ⇒ λprf.
    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    match ft_stack … pre1 with
    [ nil ⇒ (* should never happen in correct programs *)
      [id]
    | cons _ stack' ⇒
      id :: stack'
    ]
  | cl_return ⇒ λ_.
    match ft_stack … pre1 with
    [ nil ⇒ (* should never happen in correct programs *)
      [ ]
    | cons _ stack' ⇒ stack'
    ]
  | _ ⇒ λ_.ft_stack … pre1
  ] (refl …)
].
*)

(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
(* inefficient, but used only in correctness proofs *)
let rec ft_stack_observables S st st'
  (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
match ft with
[ ft_start ⇒ 〈[ ], [ ]〉
| ft_advance st1_mid st1' pre1 _ _ ⇒
  let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
  [ cl_call ⇒ λprf.
    let id ≝ as_call_ident ? «st1_mid, prf» in
    let tr' ≝ tr @ add @ [IEVcall id] in
    〈id :: stack, tr'〉
  | cl_tailcall ⇒ λprf.
    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    match stack with
    [ nil ⇒ (* should never happen in correct programs *)
      〈[ ], tr @ add〉
    | cons f stack' ⇒
      let tr' ≝ tr @ add @ [IEVtailcall f id] in
      〈id :: stack', tr'〉
    ]
  | cl_return ⇒ λ_.
    match stack with
    [ nil ⇒ (* should never happen in correct programs *)
      〈[ ], tr @ add〉
    | cons f stack' ⇒
      let tr' ≝ tr @ add @ [IEVret f] in
      〈stack', tr'〉
    ]
  | _ ⇒ λ_.〈stack, tr @ add〉
  ] (refl …)
].

definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).

definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
λS,st1,st2,ft.
match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].

lemma ft_extend_taa_obs : ∀S,st1,st2,st3,ft,taa.
  ft_stack_observables … (ft_extend_taa S st1 st2 st3 ft taa) =
    〈ft_stack … ft, ft_observables … ft @
    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
#S #st1 #st2 #st3 #ft #taa lapply ft elim taa -st2 -st3
[ #st2 #ft >append_nil @eq_pair_fst_snd ]
#st2 #st3 #st4 #H #K #G #taa #IH #ft
whd in ⊢ (??(????%)?); >IH normalize nodelta
-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
[ #st3 #H #G
| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
  >(not_costed_no_label … G)
]
>append_nil whd in ⊢ (??(???%%)(????(??%?)));
whd in match (ft_stack_observables ????) ;
@(pair_elim' … (ft_stack_observables … ft))
>(status_class_dep_match_rewrite … K) %
qed.

lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
  ∀ft : flat_trace S st1 st2.
  ∀taa : trace_any_any S st2 st3.
  ∀H : as_execute S st3 st4.∀G.
  ft_stack_observables … (ft_advance … (ft_extend_taa … ft taa) H G) =
  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
   match as_classify … st3 return λx.as_classifier … st3 x → ? with
    [ cl_call ⇒ λprf.
      let id ≝ as_call_ident ? «st3, prf» in
      let tr' ≝ tr @ add @ [IEVcall id] in
      〈id :: ft_stack … ft, tr'〉
    | cl_tailcall ⇒ λprf.
      let id ≝ as_tailcall_ident ? «st3, prf» in
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVtailcall f id] in
        〈id :: stack', tr'〉
      ]
    | cl_return ⇒ λ_.
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVret f] in
        〈stack', tr'〉
      ]
    | _ ⇒ λ_.〈stack, tr @ add〉
    ] (refl …)).
#S #st1 #st2 #st3 #st4 #ft #taa #H #G normalize nodelta
whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
@status_class_dep_match_elim #prf
@status_class_dep_match_elim #prf'
try(@⊥ >prf in prf'; #prf' -prf destruct @False)
>ft_extend_taa_obs whd in match ft_stack; whd in match ft_observables; normalize nodelta
[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
@eq_f >associative_append @eq_f
lapply prf lapply prf' lapply (taa_end_not_costed … taa)
cases taa -st3 -st2 normalize nodelta
[1,3,5,7,9,11,13: #st2 * #prf #prf' % ]
#st2 #st2' #st3 #H' #G' #K' #taa' #K #prf #prf'
>(not_costed_no_label … K) try % >append_nil %
qed.

lemma ft_extend_taaf_obs : ∀S,st1,st2,st3,ft,taaf.
  ft_stack_observables … (ft_extend_taaf S st1 st2 st3 ft taaf) =
    〈ft_stack … ft,
     ft_observables … ft @
      if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
#S #st1 #st2 #st3 #ft #taa lapply ft cases taa -st2 -st3
[ #st2 #ft >append_nil @eq_pair_fst_snd ]
#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
whd in match ft_extend_taaf; normalize nodelta
>ft_extend_taa_advance_obs @pair_elim'
>(status_class_dep_match_rewrite … G) %
qed.

(*
lemma ft_extend_taaf_advance_obs : ∀S,st1,st2,st3,st4.
  ∀ft : flat_trace S st1 st2.
  ∀taaf : trace_any_any_free S st2 st3.
  ∀H : as_execute S st3 st4.∀G.
  ft_stack_observables … (ft_advance … (ft_extend_taaf … ft taaf) H G) =
  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
   match as_classify … st3 return λx.as_classifier … st3 x → ? with
    [ cl_call ⇒ λprf.
      let id ≝ as_call_ident ? «st3, prf» in
      let tr' ≝ tr @ add @ [IEVcall id] in
      〈id :: ft_stack … ft, tr'〉
    | cl_tailcall ⇒ λprf.
      let id ≝ as_tailcall_ident ? «st3, prf» in
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVtailcall f id] in
        〈id :: stack', tr'〉
      ]
    | cl_return ⇒ λ_.
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVret f] in
        〈stack', tr'〉
      ]
    | _ ⇒ λ_.〈stack, tr @ add〉
    ] (refl …)).
#S #st1 #st2 #st3 #st4 #ft #taaf lapply ft cases taaf
whd in match ft_extend_taaf; normalize nodelta
[ #st #ft #H #G whd in ⊢ (??%?); @pair_elim' normalize nodelta % ]
#st2 #st2' #st3 #taa' #H' #G' [2: #K' ] #ft #H #G
whd in ⊢ (??%?); >ft_extend_taa_advance_obs normalize nodelta
@(pair_elim' … (ft_stack_observables … ft)) normalize nodelta
>(status_class_dep_match_rewrite … G') normalize nodelta
@status_class_dep_match_elim #prf
@status_class_dep_match_elim #prf'
try(@⊥ >prf in prf'; #prf' -prf destruct @False)
[ >associative_append 
whd in match ft_stack; whd in match ft_observables; normalize nodelta
[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
@eq_f >associative_append @eq_f
lapply prf lapply prf' lapply G
cases taaf -st3 -st2 normalize nodelta
[1,4,7,10,13,16,19: #st2 #_ #prf #prf' % ]

>(not_costed_no_label … K) try % >append_nil %
qed.
*)