Set Implicit Arguments.
Require Import Layers.
Require Import FocusPaths.
Require Import Programs.
Require Import Erasure.
A path can be used to select a sub-value out of a value (focus) or to plug
a sub-value into a value (defocus).
Inductive select :
path ->
value ->
value ->
Prop :=
|
SelectRoot:
forall v,
select PathRoot v v
|
SelectPairLeft:
forall layer1 layer2 pi v1 v2 v,
select pi v1 v ->
select (
PathPairLeft layer1 layer2 pi) (
VPair layer1 layer2 v1 v2)
v
|
SelectPairRight:
forall layer1 layer2 pi v1 v2 v,
select pi v2 v ->
select (
PathPairRight layer1 layer2 pi) (
VPair layer1 layer2 v1 v2)
v
|
SelectRef:
forall pi v1 v l,
select pi v1 v ->
select (
PathRef pi) (
VLoc l v1)
v
|
SelectRegionCapSingleton:
forall pi v1 v,
select pi v1 v ->
select (
PathRegionCapSingleton pi) (
VRegionCap (
VCons v1 VNil))
v
.
Inductive plug :
path ->
value ->
value ->
value ->
Prop :=
|
PlugRoot:
forall v1 v2,
Plugging must respect type erasure:
erase_value v1 =
erase_value v2 ->
plug PathRoot v1 v2 v2
|
PlugPairLeft:
forall layer1 layer2 pi v1 v2 v v'1,
plug pi v1 v v'1 ->
plug (
PathPairLeft layer1 layer2 pi) (
VPair layer1 layer2 v1 v2)
v (
VPair layer1 layer2 v'1
v2)
|
PlugPairRight:
forall layer1 layer2 pi v1 v2 v v'2,
plug pi v2 v v'2 ->
plug (
PathPairRight layer1 layer2 pi) (
VPair layer1 layer2 v1 v2)
v (
VPair layer1 layer2 v1 v'2)
|
PlugRef:
forall pi v1 v v'1
l,
plug pi v1 v v'1 ->
plug (
PathRef pi) (
VLoc l v1)
v (
VLoc l v'1)
|
PlugRegionCapSingleton:
forall pi v1 v v'1,
plug pi v1 v v'1 ->
plug (
PathRegionCapSingleton pi) (
VRegionCap (
VCons v1 VNil))
v (
VRegionCap (
VCons v'1
VNil))
.
Hint Constructors select plug.
Plugging respects erasure: because the new value that is plugged into
the hole must be equal (up to erasure) to the value that used to sit
in the hole, plugging is the identity (up to erasure).
Lemma plugging_respects_erasure:
forall pi v1 v2 v'1,
plug pi v1 v2 v'1 ->
erase_value v1 =
erase_value v'1.
Proof.
induction 1; layers; congruence.
Qed.