include "RTLabs/semantics.ma".
include "common/StructuredTraces.ma".

discriminator status_class.

(* NB: we do not consider jumps in the traces of RTLabs programs. *)

inductive RTLabs_classify : state → status_class → Prop ≝
| rtla_other : ∀f,fs,m.    RTLabs_classify (State f fs m)        cl_other
| rtla_call  : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call
| rtla_ret   : ∀a,b,c,d.   RTLabs_classify (Returnstate a b c d) cl_return
.

inductive RTLabs_stmt_cost : statement → Prop ≝
| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).

inductive RTLabs_cost : state → Prop ≝
| cost_instr : ∀f,fs,m.
    RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) →
    RTLabs_cost (State f fs m).

definition RTLabs_status : genv → abstract_status ≝
λge.
  mk_abstract_status
    state
    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    RTLabs_classify
    RTLabs_cost
    (λs,s'. match s with
      [ dp s p ⇒
        match s return λs. RTLabs_classify s cl_call → ? with
        [ Callstate fd args dst stk m ⇒
          λ_. match s' with
          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
          | _ ⇒ False
          ]
        | State f fs m ⇒ λH.⊥
        | _ ⇒ λH.⊥
        ] p
      ]).
inversion H try #a try #b try #c try #d try #e try #f destruct
qed.

(* Before attempting to construct a structured trace, let's show that we can
   form flat traces with evidence that they were constructed from an execution.
   
   For now we don't consider I/O. *)


coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).

(* add I/O? *)
coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.

let corec make_flat_trace ge s
  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
  flat_trace io_out io_in ge s ≝
let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
| e_wrong m ⇒ λE. ft_wrong … s m ?
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
    >(?:is_final ????? = RTLabs_is_final s1) //
    lapply (refl ? (RTLabs_is_final s1))
    cases (RTLabs_is_final s1) in ⊢ (???% → %);
    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
    ]
  | *: #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct @refl
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E
      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
      destruct
      inversion H
      [ #a #b #c #E1 destruct
      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
      | #m #E1 destruct
      ]
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr1 #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct @refl
  ]
| whd in E:(??%?); >E in H; #H
  inversion H
  [ #a #b #c #E destruct
  | #a #b #c #d #E1 destruct
  | #m #E1 destruct
  ]
] qed.

let corec make_whole_flat_trace p s
  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
  (I:make_initial_state ??? p = OK ? s) :
  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
let ge ≝ make_global … p in
let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
| e_wrong m ⇒ λE. ⊥
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ whd in E:(??%?); >exec_inf_aux_unfold in E; 
  whd in ⊢ (??%? → ?);
  >(?:is_final ????? = RTLabs_is_final s) //
  lapply (refl ? (RTLabs_is_final s))
  cases (RTLabs_is_final s) in ⊢ (???% → %);
  [ #_ whd in ⊢ (??%? → ?); #E destruct
  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
  ]
| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
    [ #a #b #c #E1 destruct
    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
      @H1
    | #m #E1 destruct
    ]
  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
] qed.