Module RegionAllocation

Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import Programs.
Require Import ValueLists.
Require Import RawPrograms.
Require Import Typing.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Canonical.
Require Import PreliminaryLemmas.
Require Import Store.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ResourcesReconfiguration.
Require Import Monotonicity.
Require Import Closed.
Require Import InversionClassification.
Require Import Erasure.
Require Import Sigma.

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

Singleton region allocation.

Lemma singleton_region_allocation:
  forall R1 v T,
  jv R1 nil nil v T ->
  exists R2 r,
  fictitious R1 R2 /\
  jv R2 nil nil (VRegionCap (VCons v VNil)) (TyRegionCap Singleton (TyRegion r) T) /\
  jv (neutral R2) nil nil (VInhabitant v) (TyAt (TyRegion r)).

Proof.

introv wtv.
exists (allocate_singleton R1 (erase_value v)) (reglimit R1); splits.

Sub-goal 1.

eauto with allocate_singleton.

Sub-goal 2.

  eapply JVRegionCap with (R1 := allocate_singleton_R1 R1 (erase_value v)) (R2 := allocate_singleton_R2 R1 (erase_value v));
  eauto using singleton_some, member_singleton with f_equal allocate_singleton.
  econstructor; try eapply star_neutral; eauto. eapply j_rio; eauto with allocate_singleton.

Sub-goal 3.

econstructor; eauto using well_typed_closed_value with resources allocate_singleton.
Qed.

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

Group region allocation.

Lemma group_region_allocation:
  forall R1,
  exists R2 r,
  fictitious R1 R2 /\
  forall T,
  wf T ->
  jv R2 nil nil (VRegionCap VNil) (TyRegionCap Group (TyRegion r) T).

Proof.

  intros. exists (allocate_group R1) (reglimit R1). split.
  eauto with allocate_group.
  intros. econstructor; simpl; eauto with allocate_group.
    unfold member. simpl. tauto.
    eapply star_neutral.
    congruence.
Qed.

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

Group region extension, also known as adoption.

Lemma region_compatibility_extend_group:
  forall R1 R2 R r v vs,
  star R1 R2 R ->
  (forall rv, region_map R2 r rv -> some (fun v => erase_value v = rv) vs) ->
  (forall rv, region_map (extend_group R (erase_value v) r) r rv -> some (fun v => erase_value v = rv) (VCons v vs)).

Proof.

  intros.
  forwards [ ? | ? ]: region_map_extend_group_reverse; [ eassumption | idtac | idtac ];
  simpl; subst; intuition eauto with resources.
Qed.

Lemma adoption:
  forall R1 R2 R v sigma T vs,
  jv R2 nil nil (VRegionCap vs) (TyRegionCap Group sigma T) ->
  jv R1 nil nil v T ->
  star R1 R2 R ->
  exists R',
  fictitious R R' /\
  jv (neutral R') nil nil (VInhabitant v) (TyAt sigma) /\
  jv R' nil nil (VRegionCap (VCons v vs)) (TyRegionCap Group sigma T).

Proof.

  intros.
  jv_inversion.
  match goal with h: tyeq (TyRegion ?r) sigma |- _ =>
    exists (extend_group R (erase_value v) r)
  end.
  splits.

The old and new resources are in the relation rxo.

eauto using (@star_commutative resource) with resources extend_group.

v is a member of the newly extended region.

sigma. econstructor; eauto using well_typed_closed_value with resources extend_group.

We have a capability for the newly extended region.

  match goal with h: star ?R2a ?R2b R2 |- _ =>
    reconfigure R (Node (Leaf R2a) (Node (Leaf R1) (Leaf R2b)))
  end.

Add v to the list of the previous inhabitants vs.

  sigma. econstructor.
    eauto with resources extend_group.
    eauto using region_compatibility_extend_group.
    unfold member in *. simpl. intuition (subst; eauto with resources extend_group).
    eapply star_extend_group; eassumption.
    eapply j_rio; eauto using (@star_commutative resource) with resources extend_group.
    eauto with resources extend_group.
    congruence.

Qed.