Commit f385602f authored by charguer's avatar charguer

dev_xand

parent d1a95033
(* DO not use; only used during the normalization phase *)
external ( & ) : bool -> bool -> bool = "%sequand"
external ( or ) : bool -> bool -> bool = "%sequor"
- xif sans argument pour pouvoir le forcer
- xifkeep ?
- xlet_keep
let H := cfml_get_precondition tt in
xlet (... \*+ H)
- "xapp as x" pratique sur xlet
- "xapps as x" pratique sur xlet
......@@ -12,8 +19,7 @@
MAJOR TODAY
- rename xextract to xpull; and xgen to xpush.
- implement xpush.
- Sys.max_array_length
......
......@@ -3,29 +3,73 @@ Set Implicit Arguments.
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Open Scope tag_scope. (**)
(* Open Scope tag_scope.*)
(*
Ltac xcur :=
cfml_get_precondition tt.
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
let compare_min () =
(min 0 1)
(********************************************************************)
(* ** List operators *)
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
(* ** Lazy binary operators *)
Lemma lazyop_val_spec :
app lazyop_val [tt] \[] \[= 1].
Proof using.
xcf. xif. xrets~.
Qed.
(*
Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
*)
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]. xret. skip. skip. } *)
(* TODO:
xor \[= true].
with xif_base and 2 continuations
*)
{ 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? *)
}
xpulls. xif. xrets~.
Qed.
Notation "'And_' v1 `&&` F2" :=
(!If (fun H Q => (v1 = true -> F2 H Q) /\ (v1 = false -> (Ret false) H Q)))
(at level 69, v1 at level 0) : charac.
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.
......@@ -35,8 +79,25 @@ let list_ops () =
(********************************************************************)
(* TODO
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
let compare_min () =
(min 0 1)
(********************************************************************)
(* ** List operators *)
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
*)
......@@ -439,13 +500,6 @@ Proof using.
Qed.
Lemma let_fun_in_let_spec' :
app let_fun_in_let [tt]
PRE \[]
RET g ST \[ forall A (x:A), app g [x] \[] \[= x] ].
Proof using.
Abort.
Lemma let_fun_in_let_spec'' :
app let_fun_in_let [tt]
PRE \[]
POST (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
......@@ -994,54 +1048,6 @@ Abort.
(********************************************************************)
(* ** Lazy binary operators *)
Lemma lazyop_val_spec :
app lazyop_val [tt] \[] \[= 1].
Proof using.
xcf. xif. xrets~.
Qed.
(*
Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
*)
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? *)
}
xpulls. 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 *)
......
......@@ -451,9 +451,6 @@ let exp_find_inlined_primitive e oargs =
| _ -> None
let exp_is_inlined_primitive e oargs =
exp_find_inlined_primitive e oargs <> None
(*#########################################################################*)
(* ** Lifting of values *)
......@@ -518,6 +515,7 @@ let rec lift_val env e =
| Texp_constraint (e, Some ty, None) ->
let typ = lift_typ_exp loc ty.ctyp_type in
Coq_annot (aux e, typ)
| _ -> fail()
(* --uncomment for debugging
| Texp_function _ -> not_in_normal_form loc "function"
......@@ -547,7 +545,6 @@ let rec lift_val env e =
| Texp_match _ -> not_in_normal_form loc "match"
| Texp_field _ -> not_in_normal_form loc "field"
*)
| _ -> fail()
(* --todo: could be a value in a purely-functional setting
| Texp_field (e, lbl) ->
......@@ -695,7 +692,7 @@ let rec cfg_exp env e =
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| Texp_apply (funct, oargs) when exp_is_inlined_primitive funct oargs -> ret e
| Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
| Texp_function (_, pat_expr_list, partial) -> not_normal ~s:"The function involved has not been lifted properly during normalization;\n check the normalized file in _output folder.\n" ()
......
......@@ -49,7 +49,15 @@ Definition tag (t:tag_type) (A:Type) (P:A) := P.
Implicit Arguments tag [A].
(** [xtag_goal] adds the tag [tag_goal] to the characteristic
(** [xtag_add T] adds the tag [T] to the head of the goal *)
Ltac xtag_add T :=
match goal with |- ?G =>
match get_fun_arg G with (?G1,?Q) =>
match get_fun_arg G1 with (?F,?H) =>
change G with ((@tag T _ F) H Q) end end end.
(** [xtag_pre_post] adds the tag [tag_goal] to the characteristic
formula at the head of the goal.
- If there are [forall] in the head, they are introduced,
then regeneralized (this feature is useful for the
......@@ -59,24 +67,20 @@ Implicit Arguments tag [A].
- It does nothing if the tag [tag_goal] is already present.
*)
Ltac xtag_goal_core tt :=
Ltac xtag_pre_post_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => idtac
| |- @tag _ _ _ _ _ =>
match goal with |- ?G =>
match get_fun_arg G with (?G1,?Q) =>
match get_fun_arg G1 with (?F,?H) =>
change G with ((@tag tag_goal _ F) H Q) end end end
| |- @tag _ _ _ _ _ => xtag_add tag_goal
| |- forall _, _ =>
intro;
xtag_goal_core tt;
xtag_pre_post_core tt;
let x := get_last_hyp tt in
revert x
| _ => idtac
end.
Tactic Notation "xtag_goal" :=
xtag_goal_core tt.
Tactic Notation "xtag_pre_post" :=
xtag_pre_post_core tt.
(** [xuntag_goal] removes [tag_goal] from the head of the goal,
or does nothing if there is no such tag. *)
......@@ -250,19 +254,22 @@ Notation "'PRE' H 'POST' Q 'CODE' F" :=
format "'[v' '[' 'PRE' H ']' '/' '[' 'POST' Q ']' '/' '[' 'CODE' F ']' ']'")
: charac.
Notation "F 'PRE' H 'RET' x 'POST' Qx" :=
(tag tag_goal F H (fun x => Qx))
Notation "F 'PRE' H 'POST' Q" :=
(tag tag_goal F H Q)
(at level 69, only parsing) : charac.
(* TODO: decide which one to use between above and below *)
(* DEPRECATED
Notation "F 'PRE' H 'RET' x 'ST' Qx" :=
(tag tag_goal F H (fun x => Qx))
(at level 69, only parsing) : charac.
Notation "F 'PRE' H 'POST' Q" :=
(tag tag_goal F H Q)
Notation "F 'PRE' H 'RET' x 'POST' Qx" :=
(tag tag_goal F H (fun x => Qx))
(at level 69, only parsing) : charac.
*)
(********************************************************************)
......@@ -272,9 +279,10 @@ Notation "'Ret' v" :=
(!Ret (fun H Q => H ==> Q v))
(at level 69) : charac.
Notation "'Ret'' P" :=
(!Ret (fun H Q => H ==> Q (isTrue P)))
Notation "'Ret_' P" :=
(Ret (isTrue P))
(at level 69) : charac.
(* that is: (!Ret (fun H Q => H ==> Q (isTrue P)))*)
Open Scope charac.
......@@ -734,6 +742,18 @@ Notation "'IfProp' P 'Then' F1 'Else' F2" :=
(at level 69, P at level 0) : charac.
*)
(********************************************************************)
(** && and || *)
Notation "'And_' v1 `&&` F2" :=
(!If (fun H Q => (v1 = true -> F2 H Q) /\ (v1 = false -> (Ret false) H Q)))
(at level 69, v1 at level 0) : charac.
Notation "'Or_' v1 `||` F2" :=
(!If (fun H Q => (v1 = true -> (Ret true) H Q) /\ (v1 = false -> F2 H Q)))
(at level 69, v1 at level 0) : charac.
(********************************************************************)
(** Case *)
......
......@@ -628,7 +628,7 @@ Ltac xlocal_core tt ::=
to collect. *)
Tactic Notation "xpre" constr(H) :=
eapply (@local_gc_pre H); [ try xlocal | xtag_goal | ].
eapply (@local_gc_pre H); [ try xlocal | xtag_pre_post | ].
(*--------------------------------------------------------*)
......@@ -656,7 +656,7 @@ Lemma xpost_lemma : forall B Q' Q (F:~~B) H,
Proof using. intros. applys* local_weaken. Qed.
Tactic Notation "xpost" :=
eapply xpost_lemma; [ try xlocal | xtag_goal | ].
eapply xpost_lemma; [ try xlocal | xtag_pre_post | ].
Lemma fix_post : forall (B:Type) (Q':B->hprop) (F:~~B) (H:hprop) Q,
is_local F ->
......@@ -671,8 +671,8 @@ Ltac xpost_core Q :=
| _ => constr:(Q)
end in
match cfml_postcondition_is_evar tt with
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_goal | apply rel_le_refl ]
| false => apply (@fix_post _ Q'); [ try xlocal | xtag_goal | ]
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply rel_le_refl ]
| false => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | ]
end.
Tactic Notation "xpost" constr(Q) :=
......@@ -707,7 +707,7 @@ Ltac xpull_core tt :=
It calls [xclean] which is useful for cleaning up *)
Tactic Notation "xpull" :=
xpull_core tt; xtag_goal.
xpull_core tt; xtag_pre_post.
(** [xpulls] calls [xpull], assumes that this call produces
an equality at the head of the goal, and it then substitutes
......@@ -781,7 +781,7 @@ Ltac xgc_remove_hprop H :=
eapply (@local_gc_pre_on H);
[ try xlocal
| hsimpl
| xtag_goal ].
| xtag_pre_post ].
Ltac xgc_remove_core X :=
xpull_check_not_needed tt;
......@@ -795,7 +795,7 @@ Ltac xgc_keep_hprop H :=
eapply (@local_gc_pre H);
[ try xlocal
| hsimpl
| xtag_goal ].
| xtag_pre_post ].
Ltac xgc_keep_core X :=
xpull_check_not_needed tt;
......@@ -808,7 +808,7 @@ Ltac xgc_keep_core X :=
Ltac xgc_post_core :=
xpull_check_not_needed tt;
eapply local_gc_post;
[ try xlocal | | xtag_goal ].
[ try xlocal | | xtag_pre_post ].
Tactic Notation "xgc" constr(H) :=
xgc_remove_core H.
......@@ -837,7 +837,7 @@ Lemma local_gc_pre_all : forall B Q (F:~~B) H,
Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
Tactic Notation "xgc_all" :=
eapply local_gc_pre_all; [ try xlocal | xtag_goal ].
eapply local_gc_pre_all; [ try xlocal | xtag_pre_post ].
......@@ -864,7 +864,7 @@ Ltac xframe_remove_core H :=
eapply xframe_lemma with (H2 := H);
[ try xlocal
| hsimpl
| xtag_goal
| xtag_pre_post
| ].
Tactic Notation "xframe" constr(H) :=
......@@ -875,7 +875,7 @@ Ltac xframe_keep_core H :=
eapply xframe_lemma with (H1 := H);
[ try xlocal
| hsimpl
| xtag_goal
| xtag_pre_post
| ].
Tactic Notation "xframe_but" constr(H) :=
......@@ -1008,7 +1008,7 @@ Qed.
Ltac xchange_apply L cont :=
eapply xchange_lemma;
[ try xlocal | applys L | cont tt | xtag_goal ].
[ try xlocal | applys L | cont tt | xtag_pre_post ].
(* note: modif should be himpl_proj1 or himpl_proj2
---what does this mean? *)
......@@ -1025,7 +1025,7 @@ Ltac xchange_forwards L modif cont :=
Ltac xchange_with_core cont H H' :=
eapply xchange_lemma with (H1:=H) (H1':=H');
[ try xlocal | | cont tt | xtag_goal ].
[ try xlocal | | cont tt | xtag_pre_post ].
Ltac xchange_core cont E modif :=
match E with
......@@ -1344,7 +1344,7 @@ Ltac xlet_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ | cont1 tt; cont2 tt ];
xtag_goal.
xtag_pre_post.
Ltac xlet_def cont0 cont1 cont2 :=
xpull_check_not_needed tt;
......@@ -1419,7 +1419,7 @@ Ltac xlet_poly_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ intros | cont1 tt; cont2 tt ];
xtag_goal.
xtag_pre_post.
Ltac xlet_poly_def cont0 cont1 cont2 :=
xpull_check_not_needed tt;
......@@ -1554,7 +1554,7 @@ Ltac xval_pre tt :=
Ltac xval_core x Hx :=
xval_pre tt;
intros x Hx;
xtag_goal.
xtag_pre_post.
Tactic Notation "xval" "as" simple_intropattern(x) simple_intropattern(Hx) :=
xval_core x Hx.
......@@ -1569,7 +1569,7 @@ Ltac xval_anonymous_impl tt :=
revert x;
let Hx := fresh "P" x in
intros x Hx;
xtag_goal.
xtag_pre_post.
Tactic Notation "xval" :=
xval_anonymous_impl tt.
......@@ -1578,7 +1578,7 @@ Tactic Notation "xval" :=
the equality [x = v] produced by [xval]. *)
Ltac xvals_core tt :=
xval_pre tt; intro; intro_subst; xtag_goal.
xval_pre tt; intro; intro_subst; xtag_pre_post.
Tactic Notation "xvals" :=
xvals_core tt.
......@@ -1595,7 +1595,7 @@ Tactic Notation "xvals" :=
Ltac xval_st_core P x Hx :=
let E := fresh in
intros x E;
asserts Hx: (P x); [ subst x | clear E; xtag_goal ].
asserts Hx: (P x); [ subst x | clear E; xtag_pre_post ].
Ltac xval_st_impl P x Hx :=
xval_pre tt; xval_st_core P x Hx.
......@@ -1695,7 +1695,7 @@ Ltac xfun_arg0 tt :=
let f := get_last_hyp tt in
let Hf := fresh "S" f in
intros Hf;
xtag_goal.
xtag_pre_post.
Tactic Notation "xfun" :=
xfun_arg0 tt.
......@@ -1705,7 +1705,7 @@ Ltac xfun_arg1 f :=
intros f;
let Hf := fresh "S" f in
intros Hf;
xtag_goal.
xtag_pre_post.
Tactic Notation "xfun" "as" ident(f) :=
xfun_arg1 f.
......@@ -1713,7 +1713,7 @@ Tactic Notation "xfun" "as" ident(f) :=
Ltac xfun_arg2 f Hf :=
xfun_pre tt;
intros f Hf;
xtag_goal.
xtag_pre_post.
Tactic Notation "xfun" "as" ident(f) ident(Hf) :=
xfun_arg2 f Hf.
......@@ -1730,7 +1730,7 @@ Ltac xfun_spec_as f P Hf cont1 :=
assert (H: P f);
[ cont1 Hf
| clear Hf; rename H into Hf; hnf in Hf ];
xtag_goal.
xtag_pre_post.
Ltac xfun_spec_as_0 P cont :=
xfun_pre tt;
......@@ -1757,7 +1757,7 @@ Ltac xfun_spec_as_2 P f Hf cont :=
and it exploits [Hf] then clears it in order to prove the goal. *)
Ltac xfun_simpl Hf :=
intros; eapply Hf; clear Hf; xtag_goal. (* hnf first? *)
intros; eapply Hf; clear Hf; xtag_pre_post. (* hnf first? *)
Tactic Notation "xfun" constr(P) :=
xfun_spec_as_0 P ltac:(fun Hf => xfun_simpl Hf).
......@@ -1962,7 +1962,7 @@ Tactic Notation "xrets" "*" constr(Q) :=
Ltac xassert_core tt :=
xuntag tag_assert;
apply local_erase;
split; [ xtag_goal | try xok ].
split; [ xtag_pre_post | try xok ].
Ltac xassert_pre cont :=
xpull_check_not_needed tt;
......@@ -2048,7 +2048,7 @@ Ltac xif_base H cont :=
xuntag tag_if;
xif_core H;
cont tt;
xtag_goal.
xtag_pre_post.
Ltac xif_then H :=
xif_base H ltac:(fun _ => xif_post H).
......@@ -2093,7 +2093,7 @@ Ltac xfail_core tt :=
xpull_check_not_needed tt;
xuntag tag_fail;
apply local_erase;
xtag_goal.
xtag_pre_post.
Tactic Notation "xfail_no_clean" :=
xfail_core tt.
......@@ -2621,7 +2621,7 @@ Tactic Notation "xcleanpat" :=
Ltac xalias_pre tt :=
xuntag tag_alias;
apply local_erase;
xtag_goal.
xtag_pre_post.
Tactic Notation "xalias" "as" ident(x) ident(H) :=
xalias_pre tt;
......@@ -2688,13 +2688,13 @@ Ltac xcase_core H cont1 cont2 :=
xuntag tag_case; apply local_erase; split;
[ introv H; cont1 tt
| introv H; xtag_negpat H; cont2 tt ];
xtag_goal.
xtag_pre_post.
Ltac xcase_no_intros_core cont1 cont2 :=
xuntag tag_case; apply local_erase; split;
[ cont1 tt
| cont2 tt ];
xtag_goal.
xtag_pre_post.
(* TODO in the second branch:
pose mark; introv H; xtag_negpat H; gen_until_mark tt *)
......@@ -2837,7 +2837,7 @@ Tactic Notation "xmatch_case" :=
xmatch_case_core ltac:(fun _ => xmatch_case_alias ltac:(fun _ => idtac)).
Tactic Notation "xmatch_no_cases" :=
xmatch_pre ltac:(fun _ => xtag_goal).
xmatch_pre ltac:(fun _ => xtag_pre_post).
Tactic Notation "xmatch_no_alias" :=
xmatch_pre ltac:(fun _ => xmatch_cases xmatch_case_no_alias).
Tactic Notation "xmatch_no_simpl_no_alias" :=
......@@ -3136,8 +3136,8 @@ Ltac xapp_prepare_goal cont :=
let cont2 tt := instantiate; try xpull in
let inner tt :=
match cfml_get_tag tt with
| tag_apply => xuntag tag_apply; cont tt; xtag_goal
| tag_none_app => cont tt; xtag_goal
| tag_apply => xuntag tag_apply; cont tt; xtag_pre_post
| tag_none_app => cont tt; xtag_pre_post
| tag_record_new => xrecord_new
end
in
......@@ -3746,7 +3746,7 @@ Ltac xcf_core_app_exploit H :=
try solve_type;
clear H;
xcf_post tt;
xtag_goal.
xtag_pre_post.
(* old: match type of H with | @tag tag_top_fun _ _ => *)
......@@ -3825,7 +3825,7 @@ Ltac xcf_show_core H :=
end in
xcf_find f;
xcf_show_name f H;
xtag_goal.
xtag_pre_post.
Tactic Notation "xcf_show" "as" ident(H) :=
xcf_show_core H.
......
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