Commit 3cc1c795 authored by charguer's avatar charguer
Browse files

batchedqueues

parent 0906883b
......@@ -15,9 +15,15 @@ struct
| [],r -> (List.rev r, [])
| q -> q
let snoc ((f,r) : 'a queue) x =
let push ((f,r) : 'a queue) x =
checkf (f, x::r)
let pop : 'a queue -> ('a * 'a queue) = function
| [], _ -> raise EmptyStructure
| x::f, r -> (x, checkf (f,r))
(* alternative: *)
let head : 'a queue -> 'a = function
| [], _ -> raise EmptyStructure
| x::f, r -> x
......
......@@ -18,22 +18,17 @@ Definition inv A (q:queue A) (Q:list A) :=
(** automation *)
Hint Unfold inv.
Hint Constructors Forall2.
Hint Resolve Forall2_last.
Ltac auto_tilde ::= eauto.
(** useful facts *)
(** verification *)
Section Polymorphic.
Variables (A: Type).
Lemma empty_spec :
Lemma empty_spec : forall A,
inv (@empty A) (@nil A).
Proof.
hnf. lets H: empty_cf. hnf in H. rewrite H.
auto.
(* todo arthur: fix display of top_label, and fix tactic below *)
intros. rewrite~ empty_cf.
Qed.
Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
......@@ -41,61 +36,46 @@ Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
Lemma is_empty_spec : forall A,
Spec is_empty (q:queue A) |R>> forall Q,
inv q Q ->
R [] (fun b => [b = bool_of (Q = nil)]).
R [] (fun b => [b = isTrue (Q = nil)]).
Proof.
....
xcf. skip. intros.
xcf.
intros (f0,r0) l [H M]. xgo.
rewrite~ M in H. inverts~ H.
intro_subst_hyp. inverts H as K.
destruct (nil_eq_app_rev_inv K). false.
xcf. intros (f,r) Q [H M].
xmatch; xrets. (* alternative: xgo. *)
fold_bool; rew_refl. (* todo: have a tactic for this *) rewrite~ M in H.
fold_bool; rew_refl. intros E. rewrite E in H.
destruct (nil_eq_app_rev_inv H). false.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
Lemma checkf_spec :
Spec checkf (q:queue a) |R>>
forall Q, (let (f,r) := q in rep (f ++ rev r) Q) ->
R (Q ;- queue a).
(* TO COMPLETE
Lemma checkf_spec : forall A,
Spec checkf (q:queue A) |R>> forall Q,
(let (f,r) := q in Q = (f ++ rev r)) ->
R [] (fun q' => [inv q' Q]).
Proof.
xcf. intros (f,r) l K. xgo; rew_list in K.
simpl. rew_list~. split; auto_false.
(* use rew_list somewhere *)
Qed.
Hint Extern 1 (RegisterSpec checkf) => Provide checkf_spec.
Lemma snoc_spec :
RepTotal snoc (Q;queue a) (X;a) >> (Q & X) ;- queue a.
Lemma pop_spec : forall A,
Spec pop (q:queue A) |R>>
forall Q, inv q Q -> Q <> nil ->
R [] (fun p => let '(x,q') := p in Hexists Q',
[Q = x::Q' /\ inv q' Q']).
Proof.
xcf. intros [f r] x. introv [H M] RX. simpl in H. xgo~.
rewrite~ app_rev_cons. ximpl~.
Qed.
Hint Extern 1 (RegisterSpec snoc) => Provide snoc_spec.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
Lemma head_spec :
RepSpec head (Q;queue a) |R>>
Q <> nil -> R (is_head Q ;; a).
Lemma push_spec :
Proof.
xcf. intros [f r] q. introv [H M] NE. xgo; rew_list in H.
rewrite~ M in H. inverts~ H.
inverts~ H.
Qed.
Hint Extern 1 (RegisterSpec head) => Provide head_spec.
Lemma tail_spec :
RepSpec tail (Q;queue a) |R>>
Q <> nil -> R (is_tail Q ;; queue a).
Proof.
xcf. intros [f r] q. introv [H M] NE. xmatch.
xgo. rewrite~ M in H. inverts~ H.
inverts H. xgo~. ximpl~.
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
Hint Extern 1 (RegisterSpec tail) => Provide tail_spec.
*)
End Polymorphic.
End BatchedQueueSpec.
End BatchedQueueSpec.
\ No newline at end of file
include ../Makefile.example
EXAMPLE_DIRS=\
DemoMake \
Dijkstra \
DynamicArrays \
FingerTree \
Compose \
CPSappend \
MutableLists \
BinaryTrees
BinaryTrees \
BatchedQueue
# DynamicArrays => fix credits
# Gensym \=> fix makefile
# InputOutputStreams => need xfor
# LambdaEval => does not work
......
......@@ -783,6 +783,7 @@ let rec cfg_structure_item s : cftops =
with Not_in_normal_form s ->
raise (Not_in_normal_form (s ^ " (only value can satisfy the value restriction)"))
in
let v_typed = coq_annot v typ in
let implicits =
match fvs_strict with
| [] -> []
......@@ -790,7 +791,7 @@ let rec cfg_structure_item s : cftops =
in
[ Cftop_val (x, coq_forall_types fvs_strict typ);
Cftop_coqs implicits;
Cftop_val_cf (x, fvs_strict, fvs_others, v);
Cftop_val_cf (x, fvs_strict, fvs_others, v_typed);
Cftop_coqs [register_cf x]; ]
(* term let-binding -- later *)
......
......@@ -36,6 +36,7 @@ and coq =
| Coq_tuple of coqs
| Coq_record of (var * coq) list
| Coq_tag of string * string option * coq
| Coq_annot of coq * coq
and coqs = coq list
......@@ -298,6 +299,9 @@ let value_variable n =
let coq_tag (tag : string) ?label (term : coq) =
Coq_tag (tag, label, term)
let coq_annot (term : coq) (term_type : coq) =
Coq_annot (term, term_type)
(*#########################################################################*)
......@@ -328,6 +332,7 @@ let rec string_of_coq c =
| Some x -> sprintf "(Label_create '%s)" x
in
sprintf "(%sCFPrint.tag %s %s _ %s)" "@" tag slab (aux term)
| Coq_annot (c1,c2) -> sprintf "(%s : %s)" (aux c1) (aux c2)
(** Print a typed identifier [(x:T)] *)
......@@ -421,7 +426,7 @@ and string_of_mod_typ mt =
| Mod_typ_var x ->
x
| Mod_typ_app xs ->
show_list (fun x ->x) " " xs (* todo: pb si nest ! *)
show_list (fun x ->x) " " xs (* todo: pb si nest ! *)
| Mod_typ_with_def (mt',x,c) ->
sprintf " %s with Definition %s := %s " (string_of_mod_typ mt') x (string_of_coq c)
| Mod_typ_with_mod (mt',x,y) ->
......
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