Module Traces

From compcert Require Import common.Events.
From compcert Require Import common.Values.
From compcert Require Import common.Globalenvs.
From compcert Require Import cfrontend.Clight.
From compcert Require Import lib.Integers.

From Velus Require Import Common.
From Velus Require Import Ident.
From Velus Require Import ObcToClight.Interface.

From Coq Require Import List.
Import List.ListNotations.

Import IStr.
Import OpAux.

Import Obc.Syn.

Section finite_traces.

  Variable p: Clight.program.

  Definition eventval_of_cvalue (v: cvalue): eventval :=
    match v with
    | Vint i => EVint i
    | Vlong i => EVlong i
    | Vfloat f => EVfloat f
    | Vsingle f => EVsingle f
    | Vptr _ _ => EVint Int.zero
    | Vundef => EVint Int.zero
    end.

  Definition eventval_of_value (v: value) : eventval :=
    match v with
    | Vscalar v => eventval_of_cvalue v
    | Venum n => EVint (enumtag_to_int n)
    end.

  Lemma eventval_of_cvalue_match:
    forall v t,
      wt_cvalue v t ->
      eventval_match (globalenv p)
                     (eventval_of_cvalue v)
                     (AST.type_of_chunk (type_chunk t)) v.

  Corollary eventval_of_value_match:
    forall v t,
      wt_value v t ->
      eventval_match (globalenv p)
                     (eventval_of_value v)
                     (AST.type_of_chunk (type_to_chunk t))
                     (value_to_cvalue v).

  Definition load_event_of_value (v: value) (xt: ident * type): event :=
    Event_vload (type_to_chunk (snd xt))
                (prefix_glob (fst xt))
                Ptrofs.zero (eventval_of_value v).

  Definition store_event_of_value (v: value) (xt: ident * type): event :=
    Event_vstore (type_to_chunk (snd xt))
                 (prefix_glob (fst xt))
                 Ptrofs.zero (eventval_of_value v).

  Definition load_events : list value -> list (ident * type) -> trace :=
    CommonList.map2 load_event_of_value.
  Definition store_events : list value -> list (ident * type) -> trace :=
    CommonList.map2 store_event_of_value.

  Fact load_events_nil : forall vs, load_events vs [] = [].

  Fact load_events_cons : forall v vs xt xts,
      load_events (v :: vs) (xt :: xts) = [load_event_of_value v xt] ++ load_events vs xts.

  Fact store_events_nil : forall vs, store_events vs [] = [].

  Fact store_events_cons : forall v vs xt xts,
      store_events (v :: vs) (xt :: xts) = [store_event_of_value v xt] ++ store_events vs xts.

End finite_traces.

Section infinite_traces.

  Variable ins : stream (list value).
  Variable outs : stream (list value).

  Variable xs : list (ident * type).
  Variable ys : list (ident * type).

  Hypothesis xs_ys_spec: xs <> [] \/ ys <> [].

  Hypothesis Len_ins: forall n, length (ins n) = length xs.
  Hypothesis Len_outs: forall n, length (outs n) = length ys.

  Lemma load_store_events_not_E0:
    forall n,
      load_events (ins n) xs <> E0 \/ store_events (outs n) ys <> E0.

  Program CoFixpoint mk_trace' (n: nat): traceinf' :=
    Econsinf' (load_events (ins n) xs ** store_events (outs n) ys)
              (mk_trace' (S n)) _.

  Definition mk_trace (n: nat) : traceinf :=
    traceinf_of_traceinf' (mk_trace' n).

  Lemma unfold_mk_trace: forall n,
      mk_trace n =
      (load_events (ins n) xs ** E0 ** store_events (outs n) ys)
        *** E0
        *** mk_trace (S n).

End infinite_traces.

Section Obc.
  Variable (m: method) (ins outs: stream (list value)).

  Hypothesis in_out_spec : m.(m_in) <> [] \/ m.(m_out) <> [].

  Hypothesis Len_ins : forall n, length (ins n) = length m.(m_in).
  Hypothesis Len_outs: forall n, length (outs n) = length m.(m_out).

  Program Definition trace_step (n: nat): traceinf :=
    mk_trace ins outs m.(m_in) m.(m_out) _ _ _ n.

End Obc.