Commit bfa89ad9 authored by charguer's avatar charguer

readonly

parent 7fc3c32d
......@@ -13,7 +13,9 @@ CFML := ..
# We compile only a subset of the files present in the folder
SRC :=\
ModelSep
ModelLambda \
ModelSep \
ModelRO
V := $(SRC:=.v)
......
Set Implicit Arguments.
Require Import LibCore Shared.
(* todo: rename state into heap *)
(************************************************************)
(* * Source language syntax *)
(** Representation of variables and locations *)
Definition var := int.
Definition loc := nat.
Global Opaque loc.
(** Syntax of the source language *)
Inductive val : Type :=
| val_unit : val
| val_int : int -> val
| val_var : var -> val
| val_loc : loc -> val
| val_fix : var -> var -> trm -> val
with trm : Type :=
| trm_val : val -> trm
| trm_if : val -> trm -> trm -> trm
| trm_let : var -> trm -> trm -> trm
| trm_app : val -> val -> trm
| trm_letfix : var -> var -> trm -> trm -> trm
| trm_new : val -> trm
| trm_get : val -> trm
| trm_set : val -> val -> trm.
(** Definition of capture-avoiding substitution *)
Fixpoint subst_val (y : var) (w : val) (v : val) : val :=
match v with
| val_var x => If x = y then w else v
| _ => v
end
(*
| val_unit => v
| val_int n => v
| val_loc l => v
| val_fix f x t => v (*closed*) (* If x = y \/ f = y then v else val_fix f x (subst_trm y w t) *)
*)
with subst_trm (y : var) (w : val) (t : trm) : trm :=
match t with
| trm_val v => trm_val (subst_val y w v)
| trm_if v t1 t2 => trm_if (subst_val y w v) (subst_trm y w t1) (subst_trm y w t2)
| trm_let x t1 t2 => trm_let x (subst_trm y w t1) (If x = y then t2 else subst_trm y w t2)
| trm_app v1 v2 => trm_app (subst_val y w v1) (subst_val y w v2)
| trm_letfix f x t1 t2 =>
trm_letfix f x
(If x = y \/ f = y then t1 else subst_trm y w t1)
(If f = y then t2 else subst_trm y w t2)
| trm_new v => trm_new (subst_val y w v)
| trm_get v => trm_get (subst_val y w v)
| trm_set v1 v2 => trm_set (subst_val y w v1) (subst_val y w v2)
end.
(*
Implicit Types t : trm.
Implicit Types v : val.
Implicit Types x f : var.
Implicit Types l : loc.
*)
(********************************************************************)
(* ** States *)
(*------------------------------------------------------------------*)
(* ** Representation of partial functions *)
(** Type of partial functions from A to B *)
Definition pfun (A B : Type) :=
A -> option B.
(** Finite domain of a partial function *)
Definition pfun_finite (A B : Type) (f : pfun A B) :=
exists (L : list A), forall (x:A), f x <> None -> Mem x L.
(** Disjointness of domain of two partial functions *)
Definition pfun_disjoint (A B : Type) (f1 f2 : pfun A B) :=
forall (x:A), f1 x = None \/ f2 x = None.
(** Disjoint union of two partial functions *)
Definition pfun_union (A B : Type) (f1 f2 : pfun A B) :=
fun (x:A) => match f1 x with
| Some y => Some y
| None => f2 x
end.
(*------------------------------------------------------------------*)
(** Representation of state *)
Section State.
(** Representation of heaps *)
Inductive state : Type := state_of {
state_data :> pfun loc val;
state_finite : pfun_finite state_data }.
Implicit Arguments state_of [].
(** Disjoint states *)
Definition state_disjoint (h1 h2 : state) : Prop :=
pfun_disjoint h1 h2.
Definition state_disjoint_3 h1 h2 h3 :=
state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3.
(** Finiteness of union *)
Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B),
pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2).
Proof using.
introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M.
specializes F1 x. specializes F2 x. unfold pfun_union in M.
apply Mem_app_or. destruct~ (f1 x).
Qed.
(** Union of states *)
Program Definition state_union (h1 h2 : state) : state :=
state_of (pfun_union h1 h2) _.
Next Obligation. destruct h1. destruct h2. apply~ pfun_union_finite. Qed.
(** Empty state *)
Program Definition state_empty : state :=
state_of (fun l => None) _.
Next Obligation. exists (@nil loc). auto_false. Qed.
(** Singleton state *)
Program Definition state_single (l:loc) (v:val) : state :=
state_of (fun l' => If l = l' then Some v else None) _.
Next Obligation.
exists (l::nil). intros. case_if. subst~.
Qed.
End State.
Implicit Arguments state_of [].
Notation "\# h1 h2" := (state_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope.
Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity)
: state_scope.
Notation "h1 \+ h2" := (state_union h1 h2)
(at level 51, right associativity) : state_scope.
(************************************************************)
(* * Source language semantics *)
Section Red.
Local Open Scope state_scope.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_val : forall m v,
red m (trm_val v) m v
| red_if : forall m1 m2 v r t1 t2,
red m1 (If v = val_int 0 then t2 else t1) m2 r ->
red m1 (trm_if v t1 t2) m2 r
| red_let : forall m1 m2 m3 x t1 t2 v1 r,
red m1 t1 m2 v1 ->
red m2 (subst_trm x v1 t2) m3 r ->
red m1 (trm_let x t1 t2) m3 r
| red_app : forall m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
red m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
red m1 (trm_app v1 v2) m2 r
| red_fix : forall m1 m2 f x t1 t2 r,
red m1 (subst_trm f (val_fix f x t1) t2) m2 r ->
red m1 (trm_letfix f x t1 t2) m2 r
| red_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
red ma (trm_new v) (ma \+ mb) (val_loc l)
| red_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
red (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| red_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
red (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Red.
Local Open Scope state_scope.
(*------------------------------------------------------------------*)
(* ** Properties on states *)
(** Symmetry of disjointness *)
Lemma pfun_disjoint_sym : forall (A B : Type),
sym (@pfun_disjoint A B).
Proof using.
introv H. unfolds pfun_disjoint. intros z. specializes H z. intuition.
Qed.
(** Commutativity of disjoint union *)
Tactic Notation "cases" constr(E) := (* TODO: move *)
let H := fresh "Eq" in cases E as H.
Lemma pfun_union_comm : forall (A B : Type) (f1 f2 : pfun A B),
pfun_disjoint f1 f2 ->
pfun_union f1 f2 = pfun_union f2 f1.
Proof using.
introv H. extens. intros x. unfolds pfun_disjoint, pfun_union.
specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false.
Qed.
(** Proving states equals *)
Lemma state_eq : forall (f1 f2: loc -> option val) F1 F2,
(forall x, f1 x = f2 x) ->
state_of f1 F1 = state_of f2 F2.
Proof using.
introv H. asserts: (f1 = f2). extens~. subst.
fequals. (* note: involves proof irrelevance *)
Qed.
(*------------------------------------------------------------------*)
(* ** Properties on states *)
(** Disjointness *)
Lemma state_disjoint_sym : forall h1 h2,
state_disjoint h1 h2 -> state_disjoint h2 h1.
Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed.
Lemma state_disjoint_comm : forall h1 h2,
\# h1 h2 = \# h2 h1.
Proof using. lets: state_disjoint_sym. extens*. Qed.
Lemma state_disjoint_empty_l : forall h,
state_disjoint state_empty h.
Proof using. intros [f F] x. simple~. Qed.
Lemma state_disjoint_empty_r : forall h,
state_disjoint h state_empty.
Proof using. intros [f F] x. simple~. Qed.
Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r.
Lemma state_disjoint_union_eq_r : forall h1 h2 h3,
state_disjoint h1 (state_union h2 h3) =
(state_disjoint h1 h2 /\ state_disjoint h1 h3).
Proof using.
intros [f1 F1] [f2 F2] [f3 F3].
unfolds state_disjoint, state_union. simpls.
unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2].
split; intros x; specializes M x;
destruct (f2 x); intuition; tryfalse.
intros x. specializes M1 x. specializes M2 x.
destruct (f2 x); intuition.
Qed.
Lemma state_disjoint_union_eq_l : forall h1 h2 h3,
state_disjoint (state_union h2 h3) h1 =
(state_disjoint h1 h2 /\ state_disjoint h1 h3).
Proof using.
intros. rewrite state_disjoint_comm.
apply state_disjoint_union_eq_r.
Qed.
Lemma state_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
(** Union *)
Lemma state_union_neutral_l : forall h,
state_union state_empty h = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
apply~ state_eq.
Qed.
Lemma state_union_neutral_r : forall h,
state_union h state_empty = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
apply state_eq. intros x. destruct~ (f x).
Qed.
Lemma state_union_comm : forall h1 h2,
state_disjoint h1 h2 ->
state_union h1 h2 = state_union h2 h1.
Proof using.
intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl.
intros. rewrite~ pfun_union_comm.
Qed.
Lemma state_union_assoc :
LibOperation.assoc state_union.
Proof using.
intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_union. simpls.
apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
Qed.
(** Hints and tactics *)
Hint Resolve state_union_neutral_l state_union_neutral_r.
Hint Rewrite
state_disjoint_union_eq_l
state_disjoint_union_eq_r
state_disjoint_3_unfold : rew_disjoint.
Tactic Notation "rew_disjoint" :=
autorewrite with rew_disjoint in *.
Tactic Notation "rew_disjoint" "*" :=
rew_disjoint; auto_star.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment