Commit 5b7e4812 authored by charguer's avatar charguer

PRE

parent 7be4642f
......@@ -35,19 +35,69 @@ COMPILATION
=> even better, wrap "coqc -quick" with an atomic commit of its result.
LATER
MAJOR TODAY
- record
- array
- notations for primitive ops
- loops
- mutual type defs
MAJOR NEXT
- partial application
- xabstract => rename as xgen
- record with
- when clauses
- xfocus
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
=> idea: inline the abbreviation automatically (abbreviation should not be cyclic though)
=> for now, do this encoding by hand.
- support float
MAJOR POSTPONED
- add support for pure records
=> need type information for normalization
=> how to shared typed/untyped AST
LATER
- semantics for records|arrays passed by value / passed by reference
TODO
- discuss the naming scheme
=> type t --> t_ || x'
=> var fresh x --> x12__
=> var x' --> x_prime_
=> var (++) --> plus_plus_infix_ || infix_plus_plus_
=> PB: plus_plus_infix' !
=> var x_ --> forbidden
- in print_tast and print_past, protect with parenth the infix names being bound
......@@ -59,7 +109,6 @@ LATER
- check that there are no uses of labels in source files
- support float
- make systematic use of || (rm -f $@; exit 1) in cfml calls
......
......@@ -7,33 +7,6 @@ Require Import Stdlib.
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*.
(********************************************************************)
(********************************************************************)
......@@ -51,8 +24,8 @@ Proof using.
(* demos: *)
xcf_show. skip.
xcf_show top_val_int. skip.
xcf_show top_val_int as M. skip.
xcf. skip.
xcf top_val_int. skip.
Qed.
Lemma top_val_int_list_spec :
......@@ -107,6 +80,7 @@ Axiom ret_unit_spec' : forall A (x:A),
Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.
Lemma seq_ret_unit_spec :
app seq_ret_unit [tt] \[] \[= tt].
Proof using.
......@@ -120,7 +94,7 @@ Proof using.
{ xapp3_no_simpl. }
{ xapp3. }
dup 4.
{ xseq. xapp. xapp. xsimpl~. }
{ xseq. xapp. xapp. xsimpl. auto. }
{ xapp. intro_subst. xapp. }
{ xapps. xapps. }
{ xapps. xapps~. }
......@@ -165,19 +139,20 @@ Qed.
Lemma let_fun_const_spec :
app let_fun_const [tt] \[] \[= 3].
Proof using.
xcf. dup 9.
{ xfun. apply Sf. xrets~. }
xcf. dup 10.
{ xfun. apply Sf. xtag_goal. xrets~. }
{ xfun as g. apply Sg. skip. }
{ xfun as g. xapp. xret. skip. }
{ xfun as g G. apply G. skip. }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
{ apply Sf. skip. }
{ xapp. skip. }
{ apply Sf. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
{ apply Sh. skip. }
{ apply Sh. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
{ apply H. skip. }
{ apply H. } }
{ xapp. skip. }
{ xapp. } }
{ xfun (fun g => app g [tt] \[] \[=3]).
{ xrets~. }
{ apply Sf. } }
......@@ -237,6 +212,13 @@ Proof using.
{ =>> M. xrets~. }
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.
(********************************************************************)
(* ** Let-term *)
......@@ -375,6 +357,22 @@ Qed.
(********************************************************************)
(* ** Type annotations *)
Ltac xval_anonymous_impl tt ::=
xval_pre tt;
intro;
let x := get_last_hyp tt in
revert x;
let Hx := fresh "P" x in
intros x Hx;
xtag_goal.
Lemma annot_let_spec :
app annot_let [tt] \[] \[= 3].
Proof using.
......@@ -535,7 +533,8 @@ Abort.
Lemma assert_in_seq_spec :
app assert_in_seq [tt] \[] \[= 4].
Proof using.
xcf. xlet. xassert. { xrets. } xrets. xextracts. xrets~.
xcf. xlet. xassert. { xrets. } xrets.
xextracts. xrets~.
Qed.
......@@ -675,23 +674,37 @@ let order_record () =
Require Import LibInt.
Lemma rec_partial_half_spec : forall x n,
n = 2 * x ->
app rec_partial_half [n] \[] \[= x].
Ltac xgo1_core tt :=
xgo_once tt.
Tactic Notation "x" :=
xgo1_core tt.
Tactic Notation "x" "~" :=
x; xauto~.
Tactic Notation "x" "*" :=
x; xauto*.
Lemma rec_partial_half_spec : forall k n,
n = 2 * k ->
app rec_partial_half [n] \[] \[= k].
Proof using.
=> x. induction_wf IH: (downto 0) x. xcf.
xif.
{ xrets~. }
{ xif.
{ xfail. math. }
{ xapps (x-1).
{ unfolds. skip.
(* TODO Anomaly: Z.sub is not an evaluable constant.
=> maybe because I made it opaque? *)
}
{ skip. }
{ xrets. skip. } }
}
dup 2.
{ => k. induction_wf IH: (downto 0) k. xcf.
xif.
{ xrets~. }
{ xif.
{ xfail. math. }
{ xapps (k-1).
{ unfolds. skip.
(* TODO Anomaly: Z.sub is not an evaluable constant.
=> maybe because I made it opaque? *)
}
{ skip. }
{ xrets. skip. } } } }
{ xind_skip as IH. xcf. x.
{ xgo~. }
{ x. { x. math. } { xapps (k-1). skip. x. x. skip. } } }
Qed.
......
......@@ -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
......
......@@ -46,14 +46,60 @@ Definition tag (t:tag_type) (A:Type) (P:A) := P.
Implicit Arguments tag [A].
(** [xtag_goal] 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
implementation of [xextract], for example).
- It does nothing if there is no such formula (i.e. when
there is no [tag] as head constant),
- It does nothing if the tag [tag_goal] is already present.
*)
Ltac xtag_goal_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
| |- forall _, _ =>
intro;
xtag_goal_core tt;
let x := get_last_hyp tt in
revert x
| _ => idtac
end.
Tactic Notation "xtag_goal" :=
xtag_goal_core tt.
(** [xuntag_goal] removes [tag_goal] from the head of the goal,
or does nothing if there is no such tag. *)
Ltac xuntag_goal_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Tactic Notation "xuntag_goal" :=
xuntag_goal_core tt.
(** [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)
| |- @tag ?t _ _ _ _ => constr:(t)
| |- app ?f ?xs ?H ?Q => constr:(tag_none_app)
| |- _ => constr:(tag_none)
let G :=
match goal with
| |- @tag tag_goal _ ?F _ _ => constr:(F)
| |- ?G => constr:(G)
end in
match G with
| @tag ?t _ _ => constr:(t)
| @tag ?t _ _ _ _ => constr:(t)
| app ?f ?xs ?H ?Q => constr:(tag_none_app)
| _ => constr:(tag_none)
end.
(** [cfml_check_not_tagged tt] fails if the head of the goal contains a tag *)
......@@ -71,10 +117,7 @@ Ltac cfml_check_not_tagged tt :=
To remove only [tag_goal], use [xuntag_goal]. *)
Ltac xuntag_core T :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end;
xuntag_goal;
match goal with
| |- @tag T _ _ => unfold tag at 1
| |- @tag T _ _ _ _ => unfold tag at 1
......@@ -85,9 +128,11 @@ Tactic Notation "xuntag" constr(T) :=
xuntag_core T.
(** [xuntag] removes the tag at the head of the goal,
and fails if there is not tag there. *)
and fails if there is not tag there. It automatically
removes the [tag_goal] at the head, if any. *)
Tactic Notation "xuntag" :=
xuntag_goal_core tt;
match goal with
| |- @tag _ _ _ => unfold tag at 1
| |- @tag _ _ _ _ _ => unfold tag at 1
......@@ -99,36 +144,6 @@ Tactic Notation "xuntag" :=
Tactic Notation "xuntags" :=
unfold tag in *.
(** [xtag_goal] adds the tag [tag_goal] to the characteristic
formula at the head of the goal. It does nothing if there
is no such formula, or if the tag [tag_goal] is already
present. *)
Ltac xtag_goal_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
| _ => idtac
end.
Tactic Notation "xtag_goal" :=
xtag_goal_core tt.
(** [xuntag_goal] removes [tag_goal] from the head of the goal,
or does nothing if there is no such tag. *)
Ltac xuntag_goal_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Tactic Notation "xuntag_goal" :=
xuntag_goal_core tt.
(********************************************************************)
......@@ -198,19 +213,46 @@ Local Open Scope tag_scope.
(********************************************************************)
(* ** Notation for applied characteristic formulae [tag_goal] *)
Notation "'PRE' P1 '==>' 'POST' P2" :=
(@pred_le heap P1 P2) (at level 69,
format "'[v' '[' 'PRE' P1 ']' '/' '==>' '/' '[' 'POST' P2 ']' ']'" )
: charac.
Notation "'PRE' Q1 '===>' 'POST' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[v' '[' 'PRE' Q1 ']' '/' '===>' '/' '[' 'POST' Q2 ']' ']'")
: charac.
(* TODO : maybe good enough?
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 69,
format "'[v' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation " Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[v' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
*)
Notation "'PRE' H 'POST' Q 'CODE' F" :=
(@tag tag_goal _ F H Q) (at level 69,
format "'[v' '[' 'PRE' H ']' '/' '[' 'POST' Q ']' '/' '[' 'CODE' F ']' ']'")
: charac.
Notation "F 'PRE' H 'POST' Q" :=
(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.
(* TODO: decide which one to use between above and below *)
Notation "F 'PRE' H 'RET' x 'ST' Qx" :=
(F H (fun x => 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)
(at level 69, only parsing) : charac.
(********************************************************************)
......
This diff is collapsed.
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