Commit 34f4e43f authored by charguer's avatar charguer

demo3

parent 739c6c7a
......@@ -7,42 +7,25 @@ Require Import Stdlib.
Ltac xapply_core H cont1 cont2 ::=
forwards_nounfold_then H ltac:(fun K =>
match cfml_postcondition_is_evar tt with
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try xok ]
| false => eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]
end).
(** [xassert] applies to a goal of the form [(Assert F) H Q],
(or, more generally, of the form [(Seq_ (Assert F) ;; F') H Q],
in which case [xseq] is called first.).
It produces two subgoals: [F H (fun (b:bool) => \[b = true] \* H)]
and [H ==> Q tt]. The second one is discharged automatically
if [Q] is not instantiated---this is the case whenever. *)
Ltac xassert_core tt :=
xuntag tag_assert;
apply local_erase;
split; [ | try xok ].
Ltac xassert_pre cont :=
xextract_check_not_needed tt;
match cfml_get_tag tt with
| tag_assert => cont tt
| tag_seq => xseq; [ cont tt | instantiate ]
end.
Tactic Notation "xassert" :=
xassert_pre ltac:(fun _ => xassert_core tt).
Tactic Notation "xif_no_simpl" constr(Q) "as" ident(H) :=
xpost Q; xif_no_simpl as H.
Tactic Notation "xif_no_simpl" constr(Q) :=
xpost Q; xif_no_simpl.
Tactic Notation "xret" constr(Q) :=
xpost Q; xret.
Tactic Notation "xret" "~" constr(Q) :=
xret Q; xauto~.
Tactic Notation "xret" "*" constr(Q) :=
xret Q; xauto*.
Tactic Notation "xrets" constr(Q) :=
xpost Q; xrets.
Tactic Notation "xrets" "~" constr(Q) :=
xrets Q; xauto~.
Tactic Notation "xrets" "*" constr(Q) :=
xrets Q; xauto*.
......@@ -476,6 +459,212 @@ Qed.
(********************************************************************)
(* ** Fatal Exceptions *)
Lemma exn_assert_false_spec : False ->
app exn_assert_false [tt] \[] \[= tt].
Proof using.
xcf. xfail. auto.
Qed.
Lemma exn_failwith_spec : False ->
app exn_failwith [tt] \[] \[= tt].
Proof using.
xcf. xfail. auto.
Qed.
Lemma exn_raise_spec : False ->
app exn_raise [tt] \[] \[= tt].
Proof using.
xcf. xfail. auto.
Qed.
(********************************************************************)
(* ** Assertions *)
Lemma assert_true_spec :
app assert_true [tt] \[] \[= 3].
Proof using.
dup 2.
{ xcf. xassert. { xrets~. } xrets~. }
{ xcf_go~. }
Qed.
Lemma assert_pos_spec : forall (x:int),
x > 0 ->
app assert_pos [x] \[] \[= 3].
Proof using.
dup 2.
{ xcf. xassert. { xrets~. } xrets~. }
{ xcf_go~. }
Qed.
Lemma assert_same_spec : forall (x:int),
app assert_same [x x] \[] \[= 3].
Proof using.
dup 2.
{ xcf. xassert. { xrets~. } xrets~. }
{ xcf_go~. }
Qed.
Lemma assert_let_spec :
app assert_let [tt] \[] \[= 3].
Proof using.
dup 2.
{ xcf. xassert. { xvals. xrets~. } xrets~. }
{ xcf_go~. }
Qed.
Lemma assert_seq_spec :
app assert_seq [tt] \[] \[= 1].
Proof using.
xcf. xapp. xassert.
xapp. xrets.
(* assert cannot do visible side effects,
otherwise the semantics could change with -noassert *)
Abort.
Lemma assert_in_seq_spec :
app assert_in_seq [tt] \[] \[= 4].
Proof using.
xcf. xlet. xassert. { xrets. } xrets. xextracts. xrets~.
Qed.
(********************************************************************)
(* ** Conditionals *)
Lemma if_true_spec :
app if_true [tt] \[] \[= 1].
Proof using.
xcf. xif. xret. xsimpl. auto.
Qed.
Lemma if_term_spec :
app if_term [tt] \[] \[= 1].
Proof using.
xcf. xfun. xapp. xret. xextracts.
xif. xrets~.
Qed.
Lemma if_else_if_spec :
app if_else_if [tt] \[] \[= 0].
Proof using.
xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
{ xrets~. }
xapps. xif. xapps. xif. xrets~.
Qed.
Lemma if_then_no_else_spec : forall (b:bool),
app if_then_no_else [b] \[] (fun x => \[ x >= 0]).
Proof using.
xcf. xapp.
xseq. xif (Hexists n, \[n >= 0] \* r ~~> n).
{ xapp. xsimpl. math. }
{ xrets. math. }
{ (*xclean.*) xextract ;=>> P. xapp. xextracts. xsimpl. math. }
Qed.
(********************************************************************)
(* ** Lazy binary operators *)
Lemma lazyop_val_spec :
app lazyop_val [tt] \[] \[= 1].
Proof using.
xcf. xif. xrets~.
Qed.
Lemma lazyop_term_spec :
app lazyop_term [tt] \[] \[= 1].
Proof using.
xcf. xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets~. }
xapps.
xlet.
{ dup 3.
{ xif_no_simpl \[= true].
{ xclean. false. }
{ xapps. xrets~. } }
{ xif. xapps. xrets~. }
{ xgo*. subst. xclean. auto. }
(* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
}
xextracts. xif. xrets~.
Qed.
Lemma lazyop_mixex_spec :
app lazyop_mixed [tt] \[] \[= 1].
Proof using.
xcf. xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets~. }
xlet \[= true].
{ xif. xapps. xlet \[= true].
{ xif. xapps. xlet \[= true].
{ xif. xrets~. }
{ intro_subst. xrets~. } }
{ intro_subst. xrets~. } }
{ intro_subst. xif. xrets~. }
Qed.
(********************************************************************)
(* ** Evaluation order *)
Lemma order_app_spec :
app order_app [tt] \[] \[= 2].
Proof using.
xcf. xapps. xfun. xfun. xfun.
xapps. { xapps. xrets~. } xextracts.
xapps. { xassert. xapps. xrets~. xapps. xrets~. } xextracts.
xapps. { xassert. xapps. xrets~. xfun.
xrets~ (fun f => \[AppCurried f [a b] := (Ret (a + b)%I)] \* r ~~> 2). }
xextract ;=> Hf.
xapp. xrets~.
(* TODO: can we make xret guess the post?
The idea is to have [(Ret f) H ?Q] where [f:func] and [f] has a spec in hyps
to instantiate Q with [fun f => H \* \[spec of f]].
Then, the proof should just be [xgo~]. *)
Qed.
Lemma order_constr_spec :
app order_constr [tt] \[] \[= 1::1::nil].
Proof using.
xcf_go*.
Qed.
(* Details:
xcf. xapps. xfun. xfun.
xapps. { xapps. xrets~. } xextracts.
xapps. { xassert. xapps. xrets~. xrets~. } xextracts.
xrets~.
*)
Lemma order_list_spec :
app order_list [tt] \[] \[= 1::1::nil].
Proof using. xcf_go*. Qed.
Lemma order_tuple_spec :
app order_tuple [tt] \[] \[= 1::1::nil].
Proof using. xcf_go*. Qed.
(* TODO:
let order_array () =
let order_record () =
let r = ref 0 in
let g () = incr r; [] in
let f () = assert (!r = 1); 1 in
{ nb = f(); items = g() }
*)
(********************************************************************)
......@@ -571,99 +760,7 @@ Qed.
(*
(********************************************************************)
(* ** Fatal Exceptions *)
Lemma exn_assert_false () =
assert false
Proof using.
xcf.
Qed.
Lemma exn_failwith () =
failwith "ok"
Proof using.
xcf.
Qed.
exception My_exn
Lemma exn_raise () =
raise My_exn
Proof using.
xcf.
Qed.
let assert_let () =
assert (let x = true in true);
3
let assert_seq () =
let r = ref 0 in
assert (incr r; true);
!r
let assert_in_seq () =
(assert (true); 3) + 1
(********************************************************************)
(* ** Assertions *)
Lemma assert_true () =
assert true; 3
Proof using.
xcf.
Qed.
Lemma assert_pos x =
assert (x > 0); 3
Proof using.
xcf.
Qed.
Lemma assert_same (x:int) (y:int) =
assert (x = y); 3
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Conditionals *)
Lemma if_true_spec :
app if_true [tt] \[] \[= 1].
Proof using.
xcf. xif. xret. xsimpl. auto.
Qed.
Lemma if_term_spec :
app if_term [tt] \[] \[= 1].
Proof using.
xcf. xfun. xapp. xret. xextracts.
xif. xrets~.
Qed.
Lemma if_else_if_spec :
app if_else_if [tt] \[] \[= 0].
Proof using.
xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
{ xrets~. }
xapps. xif. xapps. xif. xrets~.
Qed.
Lemma if_then_no_else_spec : forall (b:bool),
app if_then_no_else [b] \[] (fun x => \[ x >= 0]).
Proof using.
xcf. xapp.
xseq. xif (Hexists n, \[n >= 0] \* r ~~> n).
{ xapp. xsimpl. math. }
{ xrets. math. }
{ (*xclean.*) xextract ;=>> P. xapp. xextracts. xsimpl. math. }.
Qed.
......@@ -779,66 +876,10 @@ and rec rec_mutual g x =
*)
(********************************************************************)
(* ** Lazy binary operators
let lazyop_val () =
if true && (false || true) then 1 else 0
let lazyop_term () =
let f x = (x = 0) in
if f 1 || f 0 then 1 else 0
let lazyop_mixed () =
let f x = (x = 0) in
if true && (f 1 || (f 0 && true)) then 1 else 0
*)
(* TODO: include demo of xpost (fun r =>\[r = 3]). *)
(********************************************************************)
(* ** Evaluation order
let order_app () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
g() + f()
let order_constr () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
(g() :: f() :: nil)
let order_array () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
[| g() ; f() |]
let order_list () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
[ g() ; f() ]
let order_tuple () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
(g(), f())
let order_record () =
let r = ref 0 in
let g () = incr r; [] in
let f () = assert (!r = 1); 1 in
{ nb = f(); items = g() }
*)
(*************************************************************************)
......
......@@ -95,8 +95,8 @@ cf: $(ML)
# Make sure TLC and CFML itself are up-to-date.
# Needed only when developing TLC and CFML. Ideally, should be removed.
@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
# @$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf
# @$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick
@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
@$(MAKE) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
......
......@@ -365,11 +365,10 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
assert (b0 = []); (* since e0 should be "&&" or "||" *)
let e1',b1 = aux ~as_value:true e1 in
let e2',b2 = aux ~as_value:true e2 in
if b2 = [] then begin
if b1 = [] && b2 = [] then begin
(* produce: let <b1> in <e1> && <e2>
let <b1> in <e1> || <e2> *)
let e' = return (Pexp_apply (e0', [(l1,e1'); (l2,e2')])) in
wrap_as_value e' b1
return (Pexp_apply (e0', [(l1,e1'); (l2,e2')])), []
end else if name = "&&" then begin
(* produce: let <b1> in if <e1'> then (let <b2> in <e2'>) else false *)
wrap_as_value (return (
......
......@@ -892,9 +892,13 @@ Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) :=
the subgoals.
*)
Ltac xapply_core H cont1 cont2 :=
forwards_nounfold_then H ltac:(fun K =>
eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]).
match cfml_postcondition_is_evar tt with
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try xok ]
| false => eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]
end).
Ltac xapply_base H :=
xextract_check_not_needed tt;
......@@ -1456,7 +1460,7 @@ Tactic Notation "xval_st" constr(P) :=
with respect to the most-general specification. Here, [P]
should take the form [fun f => spec_of_f].
When this tactic fails, try
[xfun_no_simpl P as f Sf. intros. apply Sf.]
[xfun_no_simpl P as f Sf. intros. xapp_types. apply Sf.]
- [xfun_no_simpl P] is like the above but does not attempt to
automatically exploit the most general specification for
......@@ -1680,6 +1684,33 @@ Tactic Notation "xrets" "*" :=
xrets; xauto*.
(*--------------------------------------------------------*)
(* ** [xassert] *)
(** [xassert] applies to a goal of the form [(Assert F) H Q],
(or, more generally, of the form [(Seq_ (Assert F) ;; F') H Q],
in which case [xseq] is called first.).
It produces two subgoals: [F H (fun (b:bool) => \[b = true] \* H)]
and [H ==> Q tt]. The second one is discharged automatically
if [Q] is not instantiated---this is the case whenever. *)
Ltac xassert_core tt :=
xuntag tag_assert;
apply local_erase;
split; [ | try xok ].
Ltac xassert_pre cont :=
xextract_check_not_needed tt;
match cfml_get_tag tt with
| tag_assert => cont tt
| tag_seq => xseq; [ cont tt | instantiate ]
end.
Tactic Notation "xassert" :=
xassert_pre ltac:(fun _ => xassert_core tt).
(*--------------------------------------------------------*)
(* ** [xif] *)
......@@ -3233,6 +3264,7 @@ Tactic Notation "xskip_credits" :=
*)
Ltac xgo_step tt :=
match cfml_get_tag tt with
| tag_ret => xret
......@@ -3250,7 +3282,7 @@ Ltac xgo_step tt :=
| tag_if => xif
| tag_for => fail 1
| tag_while => fail 1
| tag_assert => fail 1 (* TODO assert *)
| tag_assert => xassert
| _ =>
match goal with
| |- _ ==> _ => first [ xsimpl | fail 2 ]
......@@ -3258,10 +3290,12 @@ Ltac xgo_step tt :=
end
end.
(*
(* LATER
| tag_casewhen => fail 1
| tag_app_curried
| tag_pay*)
| tag_pay
*)
Ltac xgo_once tt :=
......
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