Require Import
Coqlib Maps.
Require Import
Utf8 Utils.
Section S.
Context {
X:
Type}.
Record state:
Type :=
mkstate {
st_nextnode:
positive;
st_code:
PTree.t X;
st_wf:
forall (
pc:
positive),
Plt pc st_nextnode \/
st_code!
pc =
None
}.
Inductive state_incr:
state ->
state ->
Prop :=
state_incr_intro:
forall (
s1 s2:
state),
Ple s1.(
st_nextnode)
s2.(
st_nextnode) ->
(
forall pc,
s1.(
st_code)!
pc =
None \/
s2.(
st_code)!
pc =
s1.(
st_code)!
pc) ->
state_incr s1 s2.
Lemma state_incr_refl:
forall s,
state_incr s s.
Proof.
Lemma state_incr_trans:
forall s1 s2 s3,
state_incr s1 s2 ->
state_incr s2 s3 ->
state_incr s1 s3.
Proof.
intros.
inv H;
inv H0.
apply state_incr_intro.
apply Ple_trans with (
st_nextnode s2);
assumption.
intros.
generalize (
H3 pc) (
H2 pc).
intuition congruence.
Qed.
Lemma incr_some :
∀
s1 s2,
state_incr s1 s2 →
∀
pc i,
s1.(
st_code) !
pc =
Some i →
s2.(
st_code) !
pc =
Some i.
Proof.
intros _ _ ( s1 & s2 ).
intros _ H pc i H'.
destruct (H pc); congruence.
Qed.
Inductive res (
A:
Type) (
s:
state):
Type :=
|
Error:
Errors.errmsg ->
res A s
|
OK:
A ->
forall (
s':
state),
state_incr s s' ->
res A s.
Implicit Arguments OK [
A s].
Implicit Arguments Error [
A s].
Definition mon (
A:
Type) :
Type :=
forall (
s:
state),
res A s.
Definition ret (
A:
Type) (
x:
A) :
mon A :=
fun (
s:
state) =>
OK x s (
state_incr_refl s).
Implicit Arguments ret [
A].
Definition error (
A:
Type) (
msg:
Errors.errmsg) :
mon A :=
fun (
s:
state) =>
Error msg.
Implicit Arguments error [
A].
Definition bind (
A B:
Type) (
f:
mon A) (
g:
A ->
mon B) :
mon B :=
fun (
s:
state) =>
match f s with
|
Error msg =>
Error msg
|
OK a s'
i =>
match g a s'
with
|
Error msg =>
Error msg
|
OK b s''
i' =>
OK b s'' (
state_incr_trans s s'
s''
i i')
end
end.
Implicit Arguments bind [
A B].
Notation "'
do'
X <-
A ;
B" := (
bind A (
fun X =>
B))
(
at level 200,
X ident,
A at level 100,
B at level 200).
Remark bind_inversion:
forall (
A B:
Type) (
f:
mon A) (
g:
A ->
mon B)
(
y:
B) (
s1 s3:
state) (
i:
state_incr s1 s3),
bind f g s1 =
OK y s3 i ->
exists x,
exists s2,
exists i1,
exists i2,
f s1 =
OK x s2 i1 /\
g x s2 =
OK y s3 i2.
Proof.
intros A B f g y s1 s3 i. unfold bind.
destruct (f s1) as [| a s' i']. inversion 1.
case_eq (g a s'). inversion 2.
intros b s'' j EQ. inversion 1.
subst. exists a; exists s'; exists i'; exists j; intuition.
Qed.
Definition handle_error (
A:
Type) (
f g:
mon A) :
mon A :=
fun (
s:
state) =>
match f s with
|
OK a s'
i =>
OK a s'
i
|
Error _ =>
g s
end.
Implicit Arguments handle_error [
A].
Operations on state
The initial state (empty CFG).
Remark init_state_wf (
nextnode:
positive):
forall pc,
Plt pc nextnode \/ (
PTree.empty X)!
pc =
None.
Proof.
intros; right; apply PTree.gempty. Qed.
Definition init_state (
nextnode:
positive) :
state :=
mkstate nextnode (
PTree.empty _) (
init_state_wf nextnode).
Adding a node with the given instruction to the CFG. Return the
label of the new node.
Remark add_instr_wf:
forall s i pc,
let n :=
s.(
st_nextnode)
in
Plt pc (
Psucc n) \/ (
PTree.set n i s.(
st_code))!
pc =
None.
Proof.
intros.
case (
peq pc n);
intro.
subst pc;
left;
apply Plt_succ.
rewrite PTree.gso;
auto.
elim (
st_wf s pc);
intro.
left.
apply Plt_trans_succ.
exact H.
right;
assumption.
Qed.
Remark add_instr_incr:
forall s i,
let n :=
s.(
st_nextnode)
in
state_incr s (
mkstate
(
Psucc n)
(
PTree.set n i s.(
st_code))
(
add_instr_wf s i)).
Proof.
constructor;
simpl.
apply Ple_succ.
intros.
destruct (
st_wf s pc).
right.
apply PTree.gso.
apply Plt_ne;
auto.
auto.
Qed.
Definition add_instr (
i:
X) :
mon positive :=
fun s =>
let n :=
s.(
st_nextnode)
in
OK n
(
mkstate (
Psucc n) (
PTree.set n i s.(
st_code))
(
add_instr_wf s i))
(
add_instr_incr s i).
Remark reserve_instr_wf:
forall s pc,
Plt pc (
Psucc s.(
st_nextnode)) \/
s.(
st_code)!
pc =
None.
Proof.
intros.
elim (
st_wf s pc);
intro.
left;
apply Plt_trans_succ;
auto.
right;
auto.
Qed.
Remark reserve_instr_incr:
forall s,
let n :=
s.(
st_nextnode)
in
state_incr s (
mkstate
(
Psucc n)
s.(
st_code)
(
reserve_instr_wf s)).
Proof.
intros; constructor; simpl.
apply Ple_succ.
auto.
Qed.
Definition reserve_instr:
mon positive :=
fun (
s:
state) =>
let n :=
s.(
st_nextnode)
in
OK n
(
mkstate (
Psucc n)
s.(
st_code) (
reserve_instr_wf s))
(
reserve_instr_incr s).
Remark update_instr_wf:
forall s n i,
Plt n s.(
st_nextnode) ->
forall pc,
Plt pc s.(
st_nextnode) \/ (
PTree.set n i s.(
st_code))!
pc =
None.
Proof.
intros.
case (
peq pc n);
intro.
subst pc;
left;
assumption.
rewrite PTree.gso;
auto.
exact (
st_wf s pc).
Qed.
Remark update_instr_incr:
forall s n i (
LT:
Plt n s.(
st_nextnode)),
s.(
st_code)!
n =
None ->
state_incr s
(
mkstate s.(
st_nextnode) (
PTree.set n i s.(
st_code))
(
update_instr_wf s n i LT)).
Proof.
intros.
constructor; simpl; intros.
apply Ple_refl.
rewrite PTree.gsspec. destruct (peq pc n). left; congruence. right; auto.
Qed.
Definition check_empty_node:
forall (
s:
state) (
n:
positive), {
s.(
st_code)!
n =
None } + {
True }.
Proof.
intros.
case (
s.(
st_code)!
n);
intros.
right;
auto.
left;
auto.
Defined.
Definition update_instr (
n:
positive) (
i:
X) :
mon unit :=
fun s =>
match plt n s.(
st_nextnode),
check_empty_node s n with
|
left LT,
left EMPTY =>
OK tt
(
mkstate s.(
st_nextnode) (
PTree.set n i s.(
st_code))
(
update_instr_wf s n i LT))
(
update_instr_incr s n i LT EMPTY)
|
_,
_ =>
Error (
Errors.msg "
Transcode.update_instr")
end.
Lemma update_instr_inv {
n:
positive} {
i:
X} {
st:
state} :
forall {
u st'
p},
update_instr n i st =
OK u st'
p →
u =
tt
∧
st'.(
st_nextnode) =
st.(
st_nextnode)
∧
st'.(
st_code) =
st.(
st_code) !
n <-
i.
Proof.
unfold update_instr.
case (
plt n st.(
st_nextnode)).
intros LT.
case (
check_empty_node st n).
intros EMPTY.
intros ()
st'
p H.
inv H.
intuition.
inversion 2.
inversion 2.
Qed.
End S.
Implicit Arguments OK [
X A s].
Implicit Arguments Error [
X A s].
Implicit Arguments ret [
X A].
Implicit Arguments error [
X A].
Implicit Arguments bind [
X A B].
Implicit Arguments handle_error [
X A].
Notation "'
do'
X <-
A ;
B" := (
bind A (
fun X =>
B))
(
at level 200,
X ident,
A at level 100,
B at level 200).