Module ReferenceAllocation

Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import Store.
Require Import RawPrograms.
Require Import Programs.
Require Import Typing.
Require Import Environments.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Monotonicity.
Require Import RegionAllocation.
Require Import Erasure.

-------------------------------------------------------------------------

Subject reduction for the allocation of a new reference.

Lemma new_reference_allocation:
  forall R1 m1 l,
  jsto R1 (Store l m1) ->
  forall R1a v T1,
  jv R1a nil nil v T1 ->
  forall R1b,
  star R1a R1b R1 ->
  exists R2a R2b R2,
  jt R2a nil nil (TVal (VLoc l v)) (TyRef T1) /\
  jsto R2 (Store (S l) (extend m1 l v)) /\
  rio R1b R2b /\
  star R2a R2b R2.

Proof.

introv [ ? ? ] ? ?. subst l.

Exhibit appropriate witnesses.

exists

R2a :=

(allocate_reference R1a (erase_value v))

R2b :=

(allocate_reference_unowned R1b)

R2 :=

(allocate_reference R1 (erase_value v)).
splits; eauto 2 with allocate_reference.

Check that the new reference is well-typed.

  econstructor.
  econstructor; eauto with resources allocate_reference.
  eapply j_rio; eauto with allocate_reference.

Check that the new store is well-typed.

  unfold jsto. simpl. intuition eauto with allocate_reference.
  rewrite transform_extend. unfold extend, patch. by_cases.
    symmetry; eauto with allocate_reference.
    eauto with allocate_reference.

Qed.