Commit 2caa6321 authored by charguer's avatar charguer
Browse files

demo

parent f61104e1
Require Import Test2.
Ltac foo ::= idtac "bar".
Locate Ltac foo.
Lemma test : True.
first [ try (fail 1); idtac "ok" | idtac ].
Ltac test F := constr:($(
first [ is_evar F; exact true
| exact false ])$).
Axiom P : nat -> Prop.
Lemma foo : (forall x:nat, P x -> True) -> True.
intros. eapply (H 3).
match goal with |- _ ?x =>
let f := test x in pose f end.
Parameter t : Type.
Definition t' := t.
......
......@@ -3,20 +3,15 @@
Set Implicit Arguments.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(* If demo *)
(**)
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end ].
(* data base demo => tlc
Definition mydatabase := True.
......@@ -31,26 +26,14 @@ Qed.
*)
Ltac get_post tt :=
match goal with |- ?E =>
match get_fun_arg E with (_,?Q) => constr:(Q)
end end.
Ltac xapp_pre cont ::=
xextractible tt;
match ltac_get_tag tt with
| tag_apply =>
let Q := get_post tt in
is_evar Q; xuntag tag_apply; cont tt
| tag_apply => xgc; [ xuntag tag_apply; cont tt | ]
| tag_let_trm => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
end.
(*
Ltac auto_tilde ::= try solve [ intros; auto with maths ].
*)
Lemma if_demo_spec :
Spec if_demo (b:bool) |B>>
B [] (fun (x:int) => [0 <= x <= 1]).
......@@ -58,9 +41,7 @@ Proof.
xcf. intros. xapp. xapps.
xseq (Hexists (x:int), r ~~> x \* [x = 0 \/ x = 1] \* s ~~> 5).
xif. xapp~. hsimpl~. xrets~.
introv C. xgc. xapps. intros M. hsimpl.
...
subst. invert~ C.
introv C. xgc. xapps. intros M. hsimpl. subst. invert C; math.
Qed.
(*
......@@ -75,6 +56,8 @@ let if_demo b =
*)
(*
(*************************************************************************)
(* Arrays as sequences *)
......@@ -86,7 +69,7 @@ Lemma array_demo_spec :
B [] (fun n => [n = 3]).
Proof.
xcf.
xapp. math. intros L (LL&LV).
xapp. xapp. hnf. math. intros L (LL&LV).
xapp. math. intros Ex.
(* xapp. math. sets_eq L': (L[2:=4]). *)
(* xapp_spec ml_array_set_named_spec. math. intros L' EL'. *)
......@@ -251,6 +234,7 @@ Qed.
*)
(*************************************************************************)
(*************************************************************************)
......@@ -557,4 +541,4 @@ Qed.
Hint Extern 1 (RegisterSpec newx) => Provide newx_spec.
*)
\ No newline at end of file
*)
......@@ -14,10 +14,6 @@
# library directory is assumed to be $CFML/local/lib/ocaml.
.PHONY: all code cf proof clean
##############################################################
......@@ -85,7 +81,7 @@ cf: $(ML)
@make COQBIN=$(COQBIN) CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j all
test:
echo $(TLC)
echo $(ML)
test2:
@make CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j test
......@@ -114,7 +110,7 @@ cf_old: $(ML)
##############################################################
# Verification proof
COQINCLUDE := -R $(CFML)/lib/coq CFML -R $(TLC) TLC -I .
COQINCLUDE := -R $(PREFIX)/lib/coq CFML -R $(TLC) TLC -I .
#include $(CFML)/lib/make/Makefile.coq
......
......@@ -345,6 +345,8 @@ Ltac hsimpl_find_credits HL cont :=
Ltac hsimpl_find_credits_post tt :=
try match goal with |- \$ _ ==> \$ _ => apply credits_le end.
(* todo: add a hook to avoid copy-paste *)
Ltac hsimpl_step tt ::=
match goal with |- ?HL ==> ?HA \* ?HN =>
match HN with
......@@ -356,12 +358,12 @@ Ltac hsimpl_step tt ::=
| _ \* _ => apply hsimpl_assoc
| heap_is_single _ _ => hsimpl_try_same tt
| Group _ _ => hsimpl_try_same tt
| ?H => hsimpl_find_same H HL
| ?H => check_noevar2 H; hsimpl_find_same H HL
| \$ _ => hsimpl_find_credits HL ltac:(hsimpl_find_credits_post)
| hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post)
| ?x ~> Id _ => check_noevar x; apply hsimpl_id
| ?x ~> _ _ => check_noevar x; apply hsimpl_id_unify
| ?H => apply hsimpl_keep
| _ => apply hsimpl_keep
end
| [] => fail 1
| _ => apply hsimpl_starify
......
......@@ -1320,6 +1320,18 @@ Ltac hsimpl_find_data_post tt :=
(* todo: better implemented in cps style ? *)
(** Maintain the goal in the form
H1 \* ... \* HN \* [] ==> HA \* HR
where HA is initially empty and accumulates elements not simplifiable
and HR contains the values that are to be cancelled out;
the last item of HR is always a [].
As long as HR is of the form H \* H', we try to match H with one of the Hi.
*)
Ltac check_noevar2 M := (* todo: merge *)
first [ has_evar M; fail 1 | idtac ].
Ltac hsimpl_step tt :=
match goal with |- ?HL ==> ?HA \* ?HN =>
match HN with
......@@ -1330,17 +1342,19 @@ Ltac hsimpl_step tt :=
| heap_is_pack _ => hsimpl_extract_exists tt
| _ \* _ => apply hsimpl_assoc
| heap_is_single _ _ => hsimpl_try_same tt
| Group _ _ => hsimpl_try_same tt
| ?H => hsimpl_find_same H HL
| hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post)
| ?x ~> Id _ => check_noevar x; apply hsimpl_id
| ?x ~> _ _ => check_noevar x; apply hsimpl_id_unify
| ?H => apply hsimpl_keep
| Group _ _ => hsimpl_try_same tt (* may fail *)
| ?H => check_noevar2 H; hsimpl_find_same H HL (* may fail *)
| hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *)
| ?x ~> Id _ => check_noevar x; apply hsimpl_id (* todo: why is this requiring a fail 2 ? *)
| ?x ~> _ _ => check_noevar x; apply hsimpl_id_unify (* todo: why is this requiring a fail 2 ? *)
| _ => apply hsimpl_keep
end
| [] => fail 1
| _ => apply hsimpl_starify
end end.
Ltac hsimpl_main tt :=
hsimpl_setup tt;
(repeat (hsimpl_step tt));
......
Require Export LibCore CFPrim CFTactics CFRep.
Open Scope heap_scope.
(*---todo move--*)
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end ].
Set Implicit Arguments.
Require Export LibInt CFSpec CFPrint.
(* todo: move to libtactics *)
Ltac is_not_evar E :=
first [ is_evar E; fail 1
| idtac ].
(********************************************************************)
(* ** Tactics *)
......@@ -159,14 +165,19 @@ Proof. auto. Qed.
(*--------------------------------------------------------*)
(* ** tools for post-conditions *)
(* TODO: deprecated *)
Ltac post_is_meta tt :=
Ltac is_evar_as_bool E :=
constr:($(first
[ is_evar E; exact true
| exact false ])$).
Ltac get_post tt :=
match goal with |- ?E =>
match get_fun_arg E with (_,?Q) =>
match Q with
| Q => constr:(false)
| _ => constr:(true)
end end end.
match get_fun_arg E with (_,?Q) => constr:(Q)
end end.
Ltac post_is_meta tt :=
let Q := get_post tt in is_evar_as_bool Q.
(*--------------------------------------------------------*)
......@@ -271,6 +282,7 @@ Tactic Notation "xisspec" :=
(*--------------------------------------------------------*)
(* ** [xlocal] *)
(* DEPRECATED
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
......@@ -279,10 +291,18 @@ Ltac xlocal_core tt ::=
| apply app_local_2
| apply app_local_3
| apply app_local_4 *) ].
*)
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end ].
(*DEPRECATED
Tactic Notation "xlocal" :=
xlocal_core tt.
*)
(*--------------------------------------------------------*)
(* ** [xcf] *)
......@@ -1545,12 +1565,6 @@ Tactic Notation "xfor" :=
Tactic Notation "xfor" constr(E) :=
xfor_pre ltac:(fun _ => xfor_intros tt; xgeneralize E).
Ltac xlocal_core tt ::=
first [ assumption
| apply local_is_local
| apply app_local_1
| match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end ].
(*--------------------------------------------------------*)
......@@ -2238,6 +2252,3 @@ Tactic Notation "xgos" "*" :=
(**************************************************)
(**************************************************)
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