include "basics/lists/list.ma".
include "joint/semantics.ma".
include "common/Executions.ma".
include "common/StructuredTraces.ma".

inductive call_ud (p: params) (globals: list ident): Type [0] ≝ 
  | up: joint_internal_function p globals → call_ud p globals    (* call *)
  | down: joint_internal_function p globals → call_ud p globals. (* return *)
  
let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
  (curr: nat) (max: nat) on fn_list: nat ≝ 
  match fn_list with
  [ nil      ⇒ max
  | cons h t ⇒ match h with
    [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
      if leb max new_stack
      then max_stacksize … t new_stack new_stack
      else max_stacksize … t new_stack max
    | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
      max_stacksize … t new_stack max
    ] 
  ].

let rec extract_list_from_tlr (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
  match tr with
  [ tlr_base s1 s2 tll        ⇒ 
    extract_list_from_tll … lg top_f … tll res
  | tlr_step s1 s2 s3 tll tlr ⇒ 
    let res' ≝ extract_list_from_tll … lg top_f … tll res in
    extract_list_from_tlr … lg top_f … tlr res'
  ]
and extract_list_from_tll (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
  match tr with
  [ tll_base ends s1 s2 tal co ⇒ 
    extract_list_from_tal … lg top_f … tal res
  ]
and extract_list_from_tal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 
  match tr with
  [ tal_base_not_return s1 s2 ex cl co ⇒ res
  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
  | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒
    extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
      (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
  | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 
    let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
      (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
    extract_list_from_tal … lg top_f … tal res'
  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
    extract_list_from_tal … lg top_f … tal res
  ].

let rec tlr_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
  ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
  extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ 
  match t1 with
  [ tlr_base st1 st1' tll1 ⇒ ?
  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
  ]
and tll_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
  extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
  match t1 with
  [ tll_base ends st1 st1' tal1 co ⇒ ?
  ]
and tal_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
  match t1 with
  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
  | tal_base_return st1 st1' ex cl ⇒ ?
  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
  ].
[ cases t2
  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
  ]
| cases t2
  [ #st2 #st2' #tll2 normalize #abs cases abs
  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
  ]
| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
  @(tal_rel_extract_equal … H2)
| cases t2 
  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    #taa * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 
      destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
      cases daemon
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    * #taa * #H * #G inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize #Hsim destruct (Hsim)
      cases daemon (* use Hind again? *)  
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
    * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
    [ * * #H3 #H2 #H4 | #H2 ]
    inversion taa in ⊢ ?;
    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize in H3; destruct (H3)
    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize in H1; destruct (H1)
    ]
  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
    * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
    [* #tl2]
    inversion taa in ⊢ ?;
    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #abs destruct (abs)
    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
      >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
      >ident_eq %
    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
    * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
    #K * #tlr2' * #L [* #tl2] 
    inversion taa in ⊢ ?;
    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
      destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq 
      (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
       * not sure yet *) cases daemon
    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
      >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
    [* #tl2]
    inversion taa in ⊢ ?;
    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
      destruct (H1)
    |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
      >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
    ]
  ] 
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
    #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
    inversion taa in ⊢ ?;
    [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
    |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #H1 destruct (H1)
    ]
  | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
    * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
    inversion taa in ⊢ ?;
    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize * * #abs destruct (abs)
    ]
  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
    #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
    [2: * #tl2]
    inversion taa in ⊢ ?;
    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 
      destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
      cases tal1 in H2;
      [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
      | #ss #sf #ex'' #cl'' normalize #abs cases abs
      | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
      | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
        normalize #abs cases abs
      | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
        cases daemon (* use induction here, but no *)
      ]
    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
    [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
      destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
      >(tlr_rel_extract_equal … H3) %
    |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
    #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
    [2: * #tl2] inversion taa in ⊢ ?;
    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
      >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
      (* look further here *)
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co'
  | #ss #fs #ex' #cl'
  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' 
  ]
  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 
]
qed.

let rec tlr_rel_max_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
  match t1 with
  [ tlr_base st1 st1' tll1 ⇒ ?
  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
  ]
and tll_rel_max_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
  match t1 with
  [ tll_base ends st1 st1' tal1 co ⇒ ?
  ]
and tal_rel_max_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
  match t1 with
  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
  | tal_base_return st1 st1' ex cl ⇒ ?
  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
  ].
[1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
|3: #Hsim >(tll_rel_extract_equal … Hsim []) %
|*: #Hsim >(tal_rel_extract_equal … Hsim []) %
]
qed.