| A monad modeling programs interacting with an abstract record allocator |
Require Import Eqdep List.
Require Import LambdaTamer.ListT.
Set Implicit Arguments.
Section AllocMonad.
Variable dom : Set.
Definition mem := list (list dom).
Section allocM.
Variable A : Set.
Definition allocM := mem -> option (mem * A).
Definition allocSpec (m : mem) (p : allocM) (spec : mem -> A -> Prop) :=
match p m with
| None => False
| Some (m', v) => spec m' v
end.
End allocM.
Section aBottom.
Variable A : Set.
Definition aBottom : allocM A :=
fun _ => None.
End aBottom.
Section aReturn.
Variable A : Set.
Variable v : A.
Definition aReturn : allocM A :=
fun m => Some (m, v).
Theorem aReturn_forward : forall m,
allocSpec m aReturn (fun m' v' => m' = m /\ v' = v).
End aReturn.
Section aBind.
Variables A B : Set.
Variable p1 : allocM A.
Variable p2 : A -> allocM B.
Definition aBind : allocM B :=
fun m =>
match p1 m with
| None => None
| Some (m', v) => p2 v m'
end.
Theorem aBind_forward : forall m spec,
allocSpec m p1 (fun m' v => allocSpec m' (p2 v) spec)
-> allocSpec m aBind spec.
Theorem aBind_backward : forall m spec,
allocSpec m aBind spec
-> allocSpec m p1 (fun m' v => allocSpec m' (p2 v) spec).
End aBind.
Section aNew.
Variable fields : list dom.
Definition aNew : allocM nat :=
fun m => Some (m ++ fields :: nil, length m).
Theorem aNew_forward : forall m,
allocSpec m aNew (fun m' v => m' = m ++ fields :: nil /\ v = length m).
End aNew.
Section aRead.
Variable addr : nat.
Variable field : nat.
Definition aRead : allocM dom :=
fun m =>
match nth_error m addr with
| error => None
| value fields =>
match nth_error fields field with
| error => None
| value v => Some (m, v)
end
end.
Variable m : mem.
Variable fields : list dom.
Variable v : dom.
Hypothesis fields_ok : nth_error m addr = value fields.
Hypothesis v_ok : nth_error fields field = value v.
Variable P : mem -> dom -> Prop.
Hypothesis P_ok : P m v.
Theorem aRead_forward : allocSpec m aRead P.
End aRead.
Section aFrame.
Variable A : Set.
Variable p : allocM A.
Variables spec1 spec2 : mem -> A -> Prop.
Theorem aFrame : forall m,
allocSpec m p spec1
-> (forall m' v, spec1 m' v -> spec2 m' v)
-> allocSpec m p spec2.
End aFrame.
End AllocMonad.
Notation "x <- m1 ; m2" := (aBind m1 (fun x => m2))
(right associativity, at level 60).
Implicit Arguments aBind_backward [dom A B p1 p2 m spec].
Ltac allocM_solver' :=
repeat progress (intuition eauto;
unfold eq_rect_r, eq_rec_r, eq_rec in *; simpl in *; subst;
try apply aReturn_forward;
try apply aBind_forward;
try apply aNew_forward;
try (eapply aRead_forward; [eauto; fail | simpl; eauto; fail | idtac]);
try match goal with
| [ H : _ |- _ ] => generalize (aBind_backward H); clear H; intro H
end).
Ltac allocM_solver :=
repeat progress (allocM_solver';
try (eapply aFrame; [allocM_solver'; fail | idtac])).