Lvc.Lowering.LinearStateType

Require Import Coqlib Errors AST Integers Linear.
Require Import Bounds Conventions Locations Stacklayout.
Require Import Smallstep Globalenvs common.Events.
Require Import Util Get StateType SmallStepRelations IL.Events.

Set Implicit Arguments.

Inductive linear_step_adapter (G:Globalenvs.Genv.t fundef unit)
  : Linear.state → Events.event → Linear.state → Prop :=
| StepAdapterTau st bv vv code rs m σ'
  : Linear.step G (State st bv vv code rs m) nil σ'
    → linear_step_adapter G (State st bv vv code rs m) EvtTau σ'
| StepAdapter σ σ' f arg res fnc
  : Linear.step G σ (Event_syscall f
                               (EVint ⊝ arg)
                               (EVint res)::nil) σ'
    → linear_step_adapter G σ (EvtExtern (ExternI fnc arg res)) σ'.

Lemma linear_reddec2 G
  : reddec2 (linear_step_adapter G).
Proof.
  hnf; intros.
  unfold normal2.
  eapply Coq.Logic.Classical_Prop.classic.
Defined.

Definition linear_result (σ:Linear.state) :=
  match σ with
  | Returnstate st rs m ⇒
    match Locmap.get (R R3) rs with
    | Values.Vint retcode ⇒ Some retcode
    | _ ⇒ None
    end
  | _ ⇒ None
  end.

Lemma list_forall_det A B (R:A→B→Prop) L L1 L2
      (Rdet: ∀ x y z, R x y → R x z → y = z)
  : list_forall2 R L L1
    → list_forall2 R L L2
    → L1 = L2.
Proof.
  intros X Y.
  general induction X; invt list_forall2; eauto.
  f_equal; eauto.
Qed.

(*
Lemma extcall_arg_det rs m sp l v v'
  : extcall_arg rs m sp l v
    -> extcall_arg rs m sp l v'
    -> v = v'.
Proof.
  intros A B.
  general induction A; invt extcall_arg; eauto.
  congruence.
Qed.
 *)
(*
Lemma extcall_arguments_det rs m sp ef a a'
  : extcall_arguments rs m sp ef a
    -> extcall_arguments rs m sp ef a'
    -> a = a'.
Proof.
  eapply list_forall_det.
  intros. general induction H; invt extcall_arg_pair; f_equal; eauto using extcall_arg_det.
Qed.
 *)

Local Ltac congr :=
  repeat match goal with
         | [ H : ?t = ?x, H' : ?t = ?y |- _ ] ⇒
           assert (x = y) by congruence; subst; clear H' || clear H
         | [ H : eval_builtin_args ?G ?rs ?sp ?m ?a ?vargs,
                 H' : eval_builtin_args ?G ?rs ?sp ?m ?a ?vargs' |- _ ]
           ⇒ eapply eval_builtin_args_determ in H; eauto; subst
(*         |  H : extcall_arguments ?rs ?m ?sp ?ef ?a, H' : extcall_arguments ?rs ?m ?sp ?ef ?a' |- _
         => eapply extcall_arguments_det in H; eauto; subst*)

         | [ H : external_call ?ef ?G ?vargs ?m ?t ?vres ?m',
                  H' : external_call ?ef ?G ?vargs ?m ?t' ?vres' ?m'' |- _ ]

           ⇒ let A := fresh "A" in
              let B := fresh "B" in
              edestruct (external_call_determ _ _ _ _ _ _ _ _ _ _ H H') as [A B];
              inv A; try (edestruct B; eauto; subst); clear H || clear H'
         | [ s := _ |- _ ] ⇒ subst s
         end.

Definition rel3_functional {A B C} (R:A→B→C→Prop) :=
  ∀ a b c c', R a b c → R a b c' → c = c'.

Lemma linear_int_det G
  : internally_deterministic (linear_step_adapter G).
Proof.
  hnf; intros.
  inv H; inv H0; eauto.
  - inv H1; inv H10; congr; clear_trivial_eqs; try now (split; eauto; congr; try congruence).

  - inv H1; inv H2; exfalso; repeat (congr; clear_trivial_eqs).
Qed.

Lemma linear_ext_det G
  : externally_determined (linear_step_adapter G).
Proof.
  hnf. intros.
  invc H; invc H0; eauto.
  - inv H1; inv H8; repeat (congr; clear_trivial_eqs);
      try now (split; eauto; congr; try congruence).
  - inv H1; inv H6; repeat (congr; clear_trivial_eqs); eauto.
Qed.

Instance LinearStateType G : StateType Linear.state :=
  @Build_StateType _ (linear_step_adapter G) linear_result (linear_reddec2 G)
                   (@linear_int_det G) (@linear_ext_det G).

Ltac single_step_linear := econstructor; econstructor; eauto.

Smpl Add single_step_linear : single_step.