Commit 63b71f6d authored by charguer's avatar charguer
Browse files

compiles

parent b751968f
Set Implicit Arguments.
Require Import LibCore Shared CFHeaps.
Require Export (* LibInt *) CFPrint.
......@@ -45,7 +46,7 @@ Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
simple_intropattern(I9) simple_intropattern(I10) :=
intros I1; introv I2 I3 I4 I5 I6 I7 I8 I9 I10.
intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10.
(* [=>>] first introduces all non-dependent variables,
then behaves as [intros]. It unfolds the head of the goal using [hnf]
......@@ -58,7 +59,7 @@ Ltac intro_nondeps_aux is_already_hnf :=
match goal with
| |- (_ -> _) => idtac
| |- (Inhab _) -> _ => intro; intro_nondeps_aux true
| |- (forall _,_) => intro ?; intro_nondeps_aux true
| |- (forall _,_) => intros ?; intro_nondeps_aux true
| |- _ =>
match is_already_hnf with
| true => idtac
......@@ -111,7 +112,7 @@ Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2)
(* ********************************************************************** *)
(** * Introduction *)
(** * Introduction
Section IntrovTest.
......@@ -256,7 +257,7 @@ Proof using.
Qed.
End IntrovTest.
*)
......@@ -341,6 +342,7 @@ Tactic Notation "xclean" :=
*)
(*--------------------------------------------------------*)
(* ** [xauto] *)
......@@ -360,6 +362,12 @@ Tactic Notation "xclean" :=
[xsimpl*] is equivalent to [xsimpl; xauto*].
*)
Ltac xok_core cont := (* see [xok] spec further *)
solve [ cbv beta; apply rel_le_refl
| apply pred_le_refl
| apply hsimpl_to_qunit; reflexivity
| hsimpl; cont tt ].
Ltac math_0 ::= xclean. (* TODO: why needed? *)
Ltac xauto_common cont :=
......@@ -380,6 +388,25 @@ Tactic Notation "xauto" "*" := xauto_star.
Tactic Notation "xauto" := xauto~.
(*--------------------------------------------------------*)
(* ** [xok] *)
(** [xok] proves a goal of the form [H ==> ?H'] or [Q ===> ?Q']
by unifying the right-hand-side with the left-hand-side.
It also tries to call [hsimpl] to see if it solves the goal.
TODO: is this last feature of [xok] useful? *)
Tactic Notation "xok" :=
xok_core ltac:(idcont).
(* [xok~] and [xok*] defined further *)
Tactic Notation "xok" "~" :=
xok_core ltac:(fun _ => xauto~).
Tactic Notation "xok" "*" :=
xok_core ltac:(fun _ => xauto*).
(*--------------------------------------------------------*)
(* ** [xsimpl] *)
......@@ -408,28 +435,6 @@ Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
hsimpl X1 X2 X3; xauto~.
(*--------------------------------------------------------*)
(* ** [xok] *)
(** [xok] proves a goal of the form [H ==> ?H'] or [Q ===> ?Q']
by unifying the right-hand-side with the left-hand-side.
It also tries to call [hsimpl] to see if it solves the goal.
TODO: is this last feature of [xok] useful? *)
Ltac xok_core cont :=
solve [ cbv beta; apply rel_le_refl
| apply pred_le_refl
| apply hsimpl_to_qunit; reflexivity
| hsimpl; cont tt ].
Tactic Notation "xok" :=
xok_core ltac:(idcont).
Tactic Notation "xok" "~" :=
xok_core ltac:(fun _ => xauto~).
Tactic Notation "xok" "*" :=
xok_core ltac:(fun _ => xauto*).
(*--------------------------------------------------------*)
(* ** [xlocal] *)
......@@ -443,8 +448,8 @@ Tactic Notation "xok" "*" :=
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| apply local_is_local
(*| apply app_local_pred --TODO fix *)
| match goal with H: is_local_pred ?S |- is_local (?S _) => apply H end ].
......@@ -527,7 +532,6 @@ Ltac xextract_core :=
Tactic Notation "xextract" :=
xextract_core; xclean.
(* TODO: need to call
(** [xextracts] calls [xextract], assumes that this call produces
an equality at the head of the goal, and it then substitutes
......@@ -1115,11 +1119,11 @@ Tactic Notation "xlet" "*" constr(Q) := xlet Q; xauto*.
Tactic Notation "xlet" "*" constr(Q) "as" simple_intropattern(x) := xlet Q as x; xauto*.
(** DEPRECATED [xlets] *).
(** DEPRECATED [xlets]
Tactic Notation "xlets" constr(Q) :=
xlet Q; [ | intro_subst ].
*)
(*--------------------------------------------------------*)
(* ** [xseq] *)
......@@ -1216,7 +1220,7 @@ Tactic Notation "xval_st" constr(P) :=
(*--------------------------------------------------------*)
(* ** [xbody] *)
(* TODO: udpate *)
(* TODO: DEPRECATED
(** [xbody] applies to a goal of the form
[H: (Body f x1 .. xN => Q) |- Spec_n f K]
......@@ -1258,10 +1262,14 @@ Tactic Notation "xbody_nointro" ident(Bf) :=
(* todo: add xuntag body *)
*)
(*--------------------------------------------------------*)
(* ** [xfun] *)
(* TODO: update:
(** [xfun P] applies to a goal of the form [LetFunc f := F1 in F].
The argument [P] is the specification for [f1], which should be
a predicate of type [func -> Prop]. Typically, [S] takes the form
......@@ -1356,6 +1364,9 @@ Tactic Notation "xfun" constr(P1) constr(P2) :=
(* TODO: support higher number of mutually recursive functions. *)
*)
(*--------------------------------------------------------*)
(* ** [xret] and [xret_no_gc] and [xrets] *)
......@@ -1388,6 +1399,16 @@ Proof using.
intros. apply~ local_erase. hsimpl. auto.
Qed.
(* Lemma used by [xret_no_gc] *)
Lemma xret_no_gc_lemma : forall B (v:B) H (Q:B->hprop),
H ==> Q v ->
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. apply~ local_erase.
Qed.
Ltac xret_core :=
first [ apply xret_lemma_unify
| eapply xret_lemma ].
......@@ -1424,15 +1445,6 @@ Tactic Notation "xret" "*" :=
(** [xret_no_gc] can be used to not introduce an existentially-
quantified heap for garbage collection. *)
(* Lemma used by [xret_no_gc] *)
Lemma xret_no_gc_lemma : forall B (v:B) H (Q:B->hprop),
H ==> Q v ->
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. apply~ local_erase.
Qed.
Tactic Notation "xret_no_gc" :=
xret_no_gc_core.
Tactic Notation "xret_no_gc" "~" :=
......@@ -1471,9 +1483,13 @@ Tactic Notation "xrets" "*" :=
very likely not fit the second branch.
Remark: [xif Q'] is equivalent to [xpost Q'; xif].
TODO: have a runtime check that the post is instantiated, else fail
(and same for xmatch).
[xif as X] allows to name [X] the hypothesis [v=true] or [v=false].
[xif Q' as X] is also valid syntax. *)
Ltac xif_post H := (* todo: cleanup *)
calc_partial_eq tt;
try fold_bool; fold_prop;
......@@ -1507,7 +1523,7 @@ Tactic Notation "xif" constr(Q) :=
Tactic Notation "xif_no_simpl" "as" ident(H) :=
xif_base H ltac:(fun _ => idtac).
Tactic Notation "xif_no_simpl" :=
let H := fresh "C" in xif_manual as H.
let H := fresh "C" in xif_no_simpl as H.
(*--------------------------------------------------------*)
......@@ -1551,10 +1567,10 @@ Lemma while_loop_cf_inv_measure :
(While F1 Do F2 Done_) H Q.
Proof using.
introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc_pre (I bi mi). xlocal.
xextract as HG. clear Hi. apply local_erase. introv LR HR.
xextract. => HG. clear Hi. apply local_erase. introv LR HR.
gen bi. induction_wf IH: (int_downto_wf 0) mi. intros.
applys (rm HR). xlet. applys Hc. simpl. xif.
xseq. applys Hs. xextract as b m' E. xapplys IH. applys E. hsimpl. hsimpl.
xseq. applys Hs. xextract. => b m' E. xapplys IH. applys E. hsimpl. hsimpl.
xret_no_gc. subst Q. hsimpl.
Qed.
......@@ -1616,8 +1632,9 @@ Lemma for_loop_cf_to_inv :
(H ==> I a \* H')
/\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))
/\ (I ((b)%Z+1) \* H' ==> Q tt)) ->
(For i = a To b Do F i _Done) H Q.
(For i = a To b Do F i Done_) H Q.
Proof.
(* TODO
introv M1 M2. apply local_erase. intros S LS HS.
tests C: (a > b).
apply (rm HS). split; intros C'. math. xret_no_gc~.
......@@ -1629,6 +1646,9 @@ Proof.
xseq. eapply Mb. math. xapply IH; auto with maths; hsimpl.
xret_no_gc. math_rewrite~ (i = b +1).
Qed.
*)
Admitted.
Lemma for_loop_cf_to_inv_gen' :
forall I H',
......@@ -1637,7 +1657,7 @@ Lemma for_loop_cf_to_inv_gen' :
(H ==> I a \* H')
/\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))) ->
(a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->
(For i = a To b Do F i _Done) H (# I ((b)%Z+1) \* H').
(For i = a To b Do F i Done_) H (# I ((b)%Z+1) \* H').
Proof. intros. applys* for_loop_cf_to_inv. Qed.
Lemma for_loop_cf_to_inv_gen :
......@@ -1647,8 +1667,11 @@ Lemma for_loop_cf_to_inv_gen :
(forall i, a <= i <= (b)%Z -> F i (I i) (# I(i+1))) ->
(a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->
(# (I ((b)%Z+1) \* H')) ===> Q ->
(For i = a To b Do F i _Done) H Q.
Proof. intros. applys* for_loop_cf_to_inv. intros C. hchange (H2 C). hchange (H3 tt). hsimpl. Qed.
(For i = a To b Do F i Done_) H Q.
Proof.
intros. applys* for_loop_cf_to_inv. intros C.
hchange (H2 C). hchange (H3 tt). hsimpl.
Qed.
Lemma for_loop_cf_to_inv_up :
......@@ -1658,7 +1681,7 @@ Lemma for_loop_cf_to_inv_up :
(H ==> I a \* H') ->
(forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) ->
((# I ((b)%Z+1) \* H') ===> Q) ->
(For i = a To b Do F i _Done) H Q.
(For i = a To b Do F i Done_) H Q.
Proof. intros. applys* for_loop_cf_to_inv. intros. math. Qed.
Ltac xfor_intros tt :=
......@@ -1980,20 +2003,20 @@ Tactic Notation "xmatch" constr(Q) :=
Ltac xspec_in_hyps_core f :=
match goal with
| H: spec f _ _ |- _ => generalize H
end
end.
Ltac xspec_app_in_hyps f :=
match goal with
| H: context [ app f _ _ _ ] |- _ => generalize H
end
end.
Ltac xspec_in_core db f :=
ltac_database_get db f.
Ltac xspec_core f :=
first [ xspec_in_hyps f
first [ xspec_in_hyps_core f
(* FUTURE: | xspec_in database_spec_credits f *)
| xspec_in database_spec f
| xspec_in_core database_spec f
| xspec_app_in_hyps f ].
Tactic Notation "xspec_in_hyps" constr(f) :=
......@@ -2022,7 +2045,7 @@ Tactic Notation "xspec_in" constr(db) :=
xspec_in db f).
Tactic Notation "xspec" :=
cfml_apply_xseq_or_xlet_then_process_function ltac:(fun f =>
xspec db f).
xspec f).
(*--------------------------------------------------------*)
......@@ -2065,8 +2088,8 @@ Tactic Notation "xspec" :=
Ltac xapp_extract_app_from_spec H :=
match goal with
| |- (spec _ _ _) -> _ => intro [_ H] (* drops the curried part *)
| |- (_) -> _ => intro H
| |- (spec _ _ _) -> _ => intros [_ H] (* drops the curried part *)
| |- (_) -> _ => intros H
end.
Ltac xspec_for_xapp H :=
......@@ -2123,9 +2146,12 @@ Ltac xapp_core H E cont :=
(* [xapp_no_simpl] implementation *)
Ltac xapp_no_simpl_core E cont :=
Ltac xapp_no_simpl_core H E cont :=
xapp_common H E xapp_xapply_no_simpl cont.
Ltac xapp_no_simpl_core_no_spec E cont :=
xapp_no_simpl_core ___ E cont.
(* [xapps] implementation *)
Ltac xapps_core H E cont :=
......@@ -2140,7 +2166,9 @@ Ltac xapps_core H E cont :=
(* [xapp as X] implementation *)
Ltac xapp_as_core E X :=
xlet as X; [ xapp E | instantiate; try xextract ].
xlet as X;
[ xapp_core ___ (>>) ltac:(fun _ => idtac) (* = xapp *)
| instantiate; try xextract ].
(* Notation for [xapp] with automation and with hints *)
......@@ -2225,17 +2253,17 @@ Tactic Notation "xapps" "*" constr(E) :=
(* Notation for [xapps_no_simpl] with automation and with hints *)
Tactic Notation "xapp_no_simpl" :=
xapp_no_simpl_core (>>) ltac:(fun _ => idtac).
xapp_no_simpl_core_no_spec (>>) ltac:(fun _ => idtac).
Tactic Notation "xapp_no_simpl" "~" :=
xapp_no_simpl_core (>>) ltac:(fun _ => xauto~).
xapp_no_simpl_core_no_spec (>>) ltac:(fun _ => xauto~).
Tactic Notation "xapp_no_simpl" "*" :=
xapp_no_simpl_core (>>) ltac:(fun _ => xauto* ).
xapp_no_simpl_core_no_spec (>>) ltac:(fun _ => xauto* ).
Tactic Notation "xapp_no_simpl" constr(E) :=
xapp_no_simpl_core E ltac:(fun _ => idtac).
xapp_no_simpl_core_no_spec E ltac:(fun _ => idtac).
Tactic Notation "xapp_no_simpl" "~" constr(E) :=
xapp_no_simpl_core E ltac:(fun _ => xauto~).
xapp_no_simpl_core_no_spec E ltac:(fun _ => xauto~).
Tactic Notation "xapp_no_simpl" "*" constr(E) :=
xapp_no_simpl_core E ltac:(fun _ => xauto* ).
xapp_no_simpl_core_no_spec E ltac:(fun _ => xauto* ).
(* Notation for [xapp as x] with automation and with hints *)
......@@ -2298,9 +2326,9 @@ Tactic Notation "xapp" "*" constr(E) "as" simple_intropattern(X) :=
Tactic Notation "xapp" "as" simple_intropattern(x) :=
xapp_as_base ___ (>>) ltac:(fun _ => idtac) x.
Tactic Notation "xapp" "~" "as" simple_intropattern(x) :=
xapp_as_base ___ (>>) ltac:(fun _ => xauto~) x.
xapp_as_base ___ (>>) ltac:(fun _ => xauto~ ) x.
Tactic Notation "xapp" "*" "as" simple_intropattern(x) :=
xapp_as_base ___ (>>) ltac:(fun _ => xauto*) x.
xapp_as_base ___ (>>) ltac:(fun _ => xauto* ) x.
*)
......@@ -2479,11 +2507,11 @@ Ltac xcf_find f :=
ltac_database_get database_cf f.
Ltac xcf_core_app_exploit H :=
sapply H instantiate; try solve_type; clear H; xcf_post tt.
sapply H; instantiate; try solve_type; clear H; xcf_post tt.
(* old: match type of H with | @tag tag_top_fun _ _ => *)
Ltac xcf_core_spec tt :=
Ltac xcf_core_spec f :=
xcf_find f;
let C := fresh "C" f in
let H := fresh "S" f in
......
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