Commit a3e2865c authored by charguer's avatar charguer
Browse files

polish

parent 0225f8ed
......@@ -13,13 +13,13 @@ let is_empty q =
| _ -> false
let check = function
| [], r -> (List.rev r, [])
| [], b -> (List.rev b, [])
| q -> q
let push (f,r) x =
check (f, x::r)
let push (f,b) x =
check (f, x::b)
let pop = function
| [], _ -> raise Not_found
| x::f, r -> (x, check (f,r))
| x::f, b -> (x, check (f,b))
......@@ -6,6 +6,9 @@ Require Import FunctionalQueue_ml.
(*******************************************************************)
(** Representation Predicate *)
(** [inv L (f,b)] asserts that [L] describes the items stored in
the queue represented as [(f,b)], from front to back. *)
Definition inv A (L:list A) (q:queue_ A) : Prop :=
let (f,b) := q in
(L = f ++ rev b)
......@@ -33,16 +36,9 @@ Lemma is_empty_spec : forall A (L:list A) q,
PRE \[]
POST (fun b => \[b = isTrue (L = nil)]).
Proof.
intros A L (f,b) [I1 I2]. xcf. dup.
(* Detailed proof *)
{ xmatch.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l.
intros E. subst. false* C. } }
(* Shorter proof *)
{ xmatch; xrets.
{ rewrite* I2 in I1. }
{ subst L. applys* app_not_empty_l. intros ->. false* C . } }
intros A L (f,b) [I1 I2]. xcf. xmatch; xrets.
{ rewrite* I2 in I1. }
{ subst L. applys* app_not_empty_l. intros ->. false* C. }
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
......@@ -67,6 +63,13 @@ Hint Extern 1 (RegisterSpec check) => Provide check_spec.
(*******************************************************************)
(** Push *)
(** Source code desugared as
[[
let push q x =
match q with (f,b) -> check (f, x::b)
]]
*)
Lemma push_spec : forall A (L:list A) q x,
inv L q ->
app push [q x]
......@@ -74,16 +77,26 @@ Lemma push_spec : forall A (L:list A) q x,
POST (fun q' => \[inv (L ++ x::nil) q']).
Proof.
intros A L [f b] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. rewrite I1.
rew_list in *. auto.
xpull. intros I'. xsimpl. subst L. rew_list in *. auto.
Qed.
(* Note: [(L ++ x::nil)] gets displayed as [L & x]. *)
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
(** Source code desugared as
[[
let pop q =
match q with
| [], _ -> raise Not_found
| x::f, b -> let x1__ = check (f,b) in (x, x1__)
]]
*)
Lemma pop_spec : forall A (L:list A) q,
inv L q ->
L <> nil ->
......
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import CFML.CFLib Stdlib CFMLAdditions.
Require Import MutableQueue_ml.
Require Import TLC.LibListZ.
Require Import CFMLAdditions.
Implicit Types n : int.
Implicit Types q : loc.
......@@ -12,11 +10,19 @@ Implicit Types q : loc.
(*******************************************************************)
(** Representation Predicate *)
Definition Queue A (L:list A) (q:t_ A) :=
(** [q ~> Queue L] is a notation of [Queue L q], a heap
predicate describing a mutable queue at location [q]
with contents [L]. *)
Definition Queue A (L:list A) (q:t_ A) : hprop :=
Hexists (f:list A) (b:list A) (n:int),
q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b /\ n = length L ].
(** Note: [q] has type ['a t] is OCaml, translated as [t_ A]
in Coq. The type [t_ A] is defined as [loc], which is
the type of memory locations in CFML. *)
(*******************************************************************)
(** Unfolding and folding of the representation predicate *)
......
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