Commit 01ae4e48 authored by charguer's avatar charguer
Browse files

xret_fixed

parent 11e082f4
Set Implicit Arguments.
Require Import LibTactics CFLib LibInt LibWf Demo_ml.
Require Import LibTactics CFHeaps CFLib LibInt LibWf Demo_ml.
(*-------------------*)
(********************************************************************)
(* ** Return *)
(* includes deoms of [xret] variants *)
Lemma ret_unit_spec :
app ret_unit [tt] \[= tt]. (* same as (# \[]). *)
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
xcf.
xcf. dup 5.
xret. xsimpl. auto.
(* demos *)
xrets. auto.
xrets*.
xret_no_gc. xsimpl. auto.
xret_no_clean. xsimpl*.
Qed.
Lemma ret_int_spec :
app ret_int [tt] \[= 3].
Proof using.
xcf.
Qed.
app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
Lemma ret_int_pair_spec :
app ret_int [tt] \[= (3,4)].
Proof using.
xcf.
Qed.
app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.
Lemma ret_poly_spec : forall A,
app ret_poly [tt] \[= @nil A].
Proof using.
xcf.
Qed.
app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.
(********************************************************************)
......@@ -47,7 +47,7 @@ Qed.
(********************************************************************)
(* ** Top-level values *)
(* includes demos of [xcf] tactics *)
(* includes demos of [xcf] variants *)
Lemma top_val_int_spec :
top_val_int = 5.
Proof using.
......@@ -278,8 +278,6 @@ Qed.
(********************************************************************)
(* ** Polymorphic functions *)
Notation "\[= V]" := (fun X => \[X = V])
(at level 40) : heap_scope.
Lemma top_fun_poly_id : forall A (x:A),
......
......@@ -573,15 +573,15 @@ Notation "Q \*+ H" :=
Notation "# H" := (fun _:unit => H)
(at level 39, H at level 99) : heap_scope.
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
(*------------------------------------------------------------------*)
(* ** Notations for advanced mode *)
(* Local Open Scope heap_scope_advanced. *)
Notation "\= V" := (fun X => \[X = V])
(at level 40) : heap_scope_advanced.
Notation "P ==>+ Q" := (pred_le P%h (heap_is_star P Q))
(at level 55) : heap_scope_advanced.
......
......@@ -49,32 +49,47 @@ Lemma add_tag : forall (T:Prop->Prop), (T = fun P:Prop => P) ->
forall (G:Prop), (T G) -> G.
Proof. intros. subst. auto. Qed.
(* DEPRECATED
(** [cfml_add_tag T] adds a tag [T] to the head of the goal *)
Ltac cfml_add_tag T :=
apply (@add_tag T (refl_equal _)).
*)
(** [cfml_get_tag tt] returns the tag at the head of the goal *)
Ltac cfml_get_tag tt :=
match goal with |- @tag ?t _ _ => constr:(t) end.
match goal with
| |- @tag ?t _ _ => constr:(t)
| |- @tag ?t _ _ _ _ => constr:(t)
end.
(** [cfml_check_not_tagged tt] fails if the head of the goal contains a tag *)
Ltac cfml_check_not_tagged tt ::=
match goal with |- @tag ?t _ _ => fail 1 | _ => idtac end.
Ltac cfml_check_not_tagged tt :=
match goal with
| |- @tag ?t _ _ => fail 1
| |- @tag ?t _ _ _ _ => fail 1
| _ => idtac
end.
(** [xuntag T] removes the tag [T] at the head of the goal,
and fails if it is not there. *)
Tactic Notation "xuntag" constr(T) :=
match goal with |- @tag T _ _ => unfold tag at 1 end.
match goal with
| |- @tag T _ _ => unfold tag at 1
| |- @tag T _ _ _ _ => unfold tag at 1
end.
(** [xuntag] removes the tag at the head of the goal,
and fails if there is not tag there. *)
Tactic Notation "xuntag" :=
match goal with |- @tag _ _ _ => unfold tag at 1 end.
match goal with
| |- @tag _ _ _ => unfold tag at 1
| |- @tag _ _ _ _ _ => unfold tag at 1
end.
(** [xuntags] removes all tags from everywhere in the goal;
useful for debugging. *)
......
......@@ -2633,8 +2633,8 @@ Ltac xcf_core_app_exploit H :=
Ltac xcf_core_spec f :=
xcf_find f;
let C := fresh "C" f in
let H := fresh "S" f in
let C := fresh "Curried" in
let H := fresh "Spec" in
intros [C H];
split;
[ clear H; try apply C (* curried part *)
......@@ -2642,7 +2642,7 @@ Ltac xcf_core_spec f :=
Ltac xcf_core_app f :=
xcf_find f;
let H := fresh "S" f in
let H := fresh "Spec" in
intros [_ H]; (* curried part not needed *)
xcf_core_app_exploit H. (* todo: might need sapply here *)
......@@ -2654,11 +2654,11 @@ Ltac xcf_top_value f :=
Ltac xcf_core tt :=
intros;
match goal with
| |- spec ?f ?n ?P => xcf_core_spec f
| |- app ?f ?xs ?H ?Q => xcf_core_app f
| |- tag tag_apply (app ?f ?xs ?H ?Q) => xuntag tag_apply; xcf_core_app f
| |- ?f = _ => xcf_top_value f
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | fail 2 ]
| |- tag tag_apply (app ?f ?xs ?H ?Q) => first [ xuntag tag_apply; xcf_core_app f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | fail 2 ]
| _ => fail 1 "need to call [xcf f; => H], where [f] is the name of the definition"
end.
......@@ -2671,7 +2671,7 @@ Tactic Notation "xcf" constr(f) :=
let H := fresh in intros H; hnf in H; revert H end.
Ltac xcf_show_name f :=
let H := fresh "S" (*f*) in intros H;
let H := fresh "Spec" in intros H;
try match type of H with tag tag_top_val _ => hnf in H end.
(* TODO: can't we make a name based on f? *)
......@@ -2693,7 +2693,6 @@ Tactic Notation "xcf_show" :=
Tactic Notation "xcf_show" constr(f) :=
xcf_find f; xcf_show_name f.
Tactic Notation "xcf" "~" := xcf; xauto_tilde.
Tactic Notation "xcf" "*" := xcf; xauto_star.
......
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