Commit e2071ceb authored by charguer's avatar charguer

xfocus

parent a619a4fb
......@@ -81,6 +81,9 @@ OTHER LANGUAGES
CODE BEAUTIFY
- better error message when calling [xapp] on a record application
in which the record is not unfocused.
- make sure that check_var is called where needed
- unify the source code in main.ml and makecmj.ml
......
......@@ -5,47 +5,107 @@ Require Import Demo_ml.
Require Import Stdlib.
Ltac get_fun_arg E ::=
match E with
| ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X => constr:((X1 X2 X3 X4 X5 X6 X7,X))
| ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X => constr:((X1 X2 X3 X4 X5 X6,X))
| ?X1 ?X2 ?X3 ?X4 ?X5 ?X => constr:((X1 X2 X3 X4 X5,X))
| ?X1 ?X2 ?X3 ?X4 ?X => constr:((X1 X2 X3 X4,X))
| ?X1 ?X2 ?X3 ?X => constr:((X1 X2 X3,X))
| ?X1 ?X2 ?X => constr:((X1 X2,X))
| ?X1 ?X => constr:((X1,X))
end.
(********************************************************************)
(* ** Records *)
type 'a sitems = {
mutable nb : int;
mutable items : 'a list; }
Lemma sitems_build_spec : forall (A:Type) (n:int),
app sitems_build [n] \[] (fun r => r ~> `{ nb' := n; items' := @nil A }).
Proof using. xcf_go~. Qed.
Lemma sitems_build n =
{ nb = n; items = [] }
Lemma sitems_get_nb_spec : forall (A:Type) (r:loc) (n:int),
app_keep sitems_get_nb [r]
(r ~> `{ nb' := n; items' := @nil A })
\[= n].
Proof using.
xcf.
Qed.
dup 3.
{ intros A. xcf_show as R. applys (R A). xgo~. }
{ xcf_show as R. unfold sitems_ in R. specializes R unit. xgo~. }
{ xcf_go~. Unshelve. solve_type. }
Qed. (* TODO: can we do better than a manual unshelve for dealing with unused type vars? *)
Lemma sitems_get_nb r =
r.nb
Lemma sitems_incr_nb_spec : forall (A:Type) (L:list A) (r:loc) (n:int),
app sitems_incr_nb [r]
(r ~> `{ nb' := n; items' := L })
(# (r ~> `{ nb' := n+1; items' := L })).
Proof using.
xcf.
dup 2.
{ xcf. xapps. xapp. Unshelve. solve_type. }
{ xcf_go*. Grab Existential Variables. solve_type. }
Qed.
Lemma sitems_incr_nb r =
r.nb <- r.nb + 1
Lemma sitems_length_item_spec : forall (A:Type) (r:loc) (L:list A) (n:int),
app_keep sitems_length_items [r]
(r ~> `{ nb' := n; items' := L })
\[= LibListZ.length L ].
Proof using.
xcf.
dup 2.
{ xcf. xapps. xrets. }
{ xcf_go*. }
Qed.
Lemma sitems_length_items r =
List.length r.items
Definition Sitems A (L:list A) r :=
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
Lemma sitems_push_spec : forall (A:Type) (r:loc) (L:list A) (x:A),
app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
Proof using.
xcf.
xcf. xunfold Sitems. xextract ;=> n E.
xapps. xapps. xapps. xapp. xsimpl. rew_list; math.
Qed.
Lemma sitems_push x r =
r.nb <- r.nb + 1;
r.items <- x :: r.items
Proof using.
xcf.
(** Demo of [xfocus] and [xunfocus] *)
Lemma Sitems_focus : forall r A (L:list A),
r ~> Sitems L ==>
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
Proof using. intros. xunfolds~ Sitems. Qed.
Lemma Sitems_unfocus : forall r A (L:list A) (n:int),
n = LibListZ.length L ->
r ~> `{ nb' := n; items' := L } ==>
r ~> Sitems L.
Proof using. intros. xunfolds~ Sitems. Qed.
Implicit Arguments Sitems_unfocus [].
Hint Extern 1 (Register focus (Sitems _)) =>
Provide Sitems_focus.
Hint Extern 1 (Register unfocus (record_repr `{ nb' := _; items' := _ }')) =>
Provide Sitems_unfocus.
(** - [xfocusx t] is short for [xfocus t; xextract]
- [xfocusx t] is short for [xfocus t; xextracts] *)
Tactic Notation "xfocusx" constr(t) :=
xfocus t; xextract.
Tactic Notation "xfocusxs" constr(t) :=
xfocus t; xextracts.
Lemma sitems_push_spec' : forall (A:Type) (r:loc) (L:list A) (x:A),
app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
Proof using.
xcf. dup 2.
{ xfocus r. xextract ;=> n E. skip. }
{ xfocusx r ;=> n E. xapps. xapps. xapps. xapp.
xunfocus r. rew_list; math. xsimpl~. }
Qed.
(********************************************************************)
(* ** Arrays *)
......
......@@ -241,21 +241,6 @@ Proof using.
destruct (in_union_inv N) as [P|P]; apply~ H.
Qed.
Tactic Notation "xfocus2" constr(x) :=
xfocus x; xfocus x.
Tactic Notation "xfocus2" "~" constr(x) :=
xfocus2 x; auto_tilde.
Tactic Notation "xfocus2" "*" constr(x) :=
xfocus2 x; auto_star.
Tactic Notation "xunfocus2" constr(x) :=
xunfocus x; xunfocus x.
Tactic Notation "xunfocus2" "~" constr(x) :=
xunfocus2 x; auto_tilde.
Tactic Notation "xunfocus2" "*" constr(x) :=
xunfocus2 x; auto_star.
(** verification *)
Lemma empty_spec : Spec empty () |R>>
......
......@@ -1105,7 +1105,11 @@ Tactic Notation "xchange" constr(E1) constr(E2) constr(E3) :=
Hint Extern 1 (Register focus (Tree _)) =>
Provide tree_focus_contents.
Then, use: [xfocus p]. *)
Then, use: [xfocus p].
Variants:
- [xfocus2 p] to perform [xfocus p] twice. Only applies when there
is no existentials to be extracted after the first [xfocus]. *)
Ltac get_refocus_args tt :=
match goal with
......@@ -1157,6 +1161,14 @@ Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropatt
*)
Tactic Notation "xfocus2" constr(x) :=
xfocus x; xfocus x.
Tactic Notation "xfocus2" "~" constr(x) :=
xfocus2 x; xauto_tilde.
Tactic Notation "xfocus2" "*" constr(x) :=
xfocus2 x; xauto_star.
(************************************************************)
(* ** [xunfocus] *)
......@@ -1176,7 +1188,13 @@ Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropatt
Hint Extern 1 (Register unfocus (Ref Id (MNode _ _ _))) =>
Provide tree_node_unfocus.
Then, use: [xunfocus p]. *)
Then, use: [xunfocus p].
Variants:
- [xunfocus p1 .. pn] to perform several unfocus operations
- [xunfocus2 p] to perform [xunfocus p] twice.
*)
Ltac xunfocus_constr t :=
match get_refocus_args tt with (?H1,?H2) =>
......@@ -1200,8 +1218,7 @@ Tactic Notation "xunfocus" "*" constr(t) :=
xunfocus t; xauto*.
(** It is often useful to chain unfocus operations.
The syntax [xunfocus p1 .. pn] is provided for that purpose. *)
(** *)
Tactic Notation "xunfocus" constr(t1) constr(t2) :=
xunfocus t1; xunfocus t2.
......@@ -1210,6 +1227,15 @@ Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) :=
Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) constr(t4) :=
xunfocus t1; xunfocus t2 t3 t4.
(** [xfocus2] *)
Tactic Notation "xunfocus2" constr(x) :=
xunfocus x; xunfocus x.
Tactic Notation "xunfocus2" "~" constr(x) :=
xunfocus2 x; xauto_tilde.
Tactic Notation "xunfocus2" "*" constr(x) :=
xunfocus2 x; xauto_star.
(*--------------------------------------------------------*)
......@@ -2514,7 +2540,7 @@ Ltac xspec_in_core db f :=
Ltac xspec_for_record f :=
match f with
| record_get => xspec_record_get_compute tt
| record_set => xspec_record_set_compute tt
| record_set => xspec_record_set_compute tt
end.
(* Note: if [f] is a record function, it needs to be the application visible in the goal *)
......
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