Commit 0646d4f0 authored by POTTIER Francois's avatar POTTIER Francois
parents 5b0ea56d 8795a784
......@@ -54,5 +54,6 @@ WHERE := $(shell $(COQBIN)coqc -where)
CONTRIB := $(WHERE)/user-contrib
install:
rm -rf $(CONTRIB)/CFML
mkdir -p $(CONTRIB)
ln -s `pwd` $(CONTRIB)/CFML
lib/stdlib should have make quick target
----------
-- lib/stdlib should have make quick target
-- while loop invariant : when b is false, should not prove decrease
......@@ -43,57 +39,48 @@ lib/stdlib should have make quick target
-- Array.iter forall l, Array xs \c I l
-- renommer Array.of_list
-- utiliser "of_list []" à la place de make_empty
-- régler le "==>"
-- utiliser "of_list []" à la place de make_empty
-- avoir un flag pour _output
-- external sur une constante, passe pas le typeur
-- ajouter
- documenter la faiblesse de Array.make
- remettre les vrais noms des external
- todo: test xif new variants
-- documenter la faiblesse de Array.make
-- remettre les vrais noms des external
-- todo: test xif new variants
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
-- todo: test xand
-- xclose with args for the change.
-- xsimpl on I X ==> I Y produces X = Y.
-- xapp_rm
-- generate inhab instance for algebraic
-- hint spec based on type args
-- xchanges
-- implement xpush.
- implement xpush.
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
----
MAJOR TODAY
----
MAJOR NEXT
- record with imperative
......@@ -124,7 +111,7 @@ MAJOR NEXT
with : match r with T_intro x1 .. xN => T_intro x1 .. yI .. xN
=> requires the order of labels to be fixed as in the definition.
----
MAJOR NEXT NEXT
- xlet_keep
......@@ -143,7 +130,10 @@ MAJOR NEXT NEXT
- see if we can get rid of make_cmj, using -only-cmj
=> make_cmj seems to already be never used.
-- xwhile: error reporting when arguments don't have the right types.
----
MAJOR POSTPONED
- support char, string, float
......@@ -224,65 +214,9 @@ MAKEFILE BEAUTIFY
##################################################################
# COQ BUG remaining
--------------
coq 8.6:
> coqc -v
The Coq Proof Assistant, version trunk (July 2016)
--------------
omega requires Z.sub to be transparent, but this is an issue for simpl.
--------------
~/shared/formalmetacoq/tuto$
coqc -R . TUTO -R ~/tlc/src TLC Coind.v -quick
Crashes if "Print foo" command remains in script.
--------------
semantics of config.keys with modifiers by group...
--------------
Warning: Notation _ * _ was already used in scope type_scope
[notation-overridden,parsing]
=> s'affiche à chaque include !
---------------
Coqide internal error: Source ID 1252 was not found when attempting to remove it
Handshake failed: End_of_file
Thread 122 killed on uncaught exception Sys.Break
=> don't know how
---------------
disable highlighting in feeback window
##############################################
I successfully migrated all my scripts to Coq 8.6, without pain.
I've reported a couple of bugs in the bugtracker. Most interesting ones:
- coqide is even slower than it used to, and is up to 4.5x slower than coqc (#4935).
- coqide interrupt button no longer works, it only kills the parser thread (#4700),
- forcing to use "Arguments" vs "Implicit Arguments" is problematic imo,
because "Arguments" requires too much redundant information (#4936).
Regarding compilation speeed, I confirm that v8.6 is a little bit
faster than v8.5, typically around 10% faster for my scripts,
and sometimes up to 25%, depending on the file. Details follow.
......@@ -356,166 +290,11 @@ v8.6:
##############################################
---------------
CFML/lib/CFHeaps.v
v8.5
time coqc CFHeaps.vo
real 0m12.192s
coqide
~ 14s
v8.6
time coqc CFHeaps.vo
real 0m8.782s
coqide
~ 19s
---------------
To reproduce, use the following branch that compiles both in 8.5 and 8.6:
git clone -b coq-v8.6 https://gforge.inria.fr/git/tlc/tlc.git
Run "make" (to produce vio), or "export SERIOUS=1; make" (to produce vo).
---------------
TLC/LibList.v
v8.5
time coqc
real 0m8.202s
coqide
~ 20s
v8.6
time coqc
real 0m7.787s
coqide
~ 32s
---------------
To reproduce, use the following branch that compiles both in 8.5 and 8.6:
git clone -b coq-v8.6 https://gforge.inria.fr/git/tlc/tlc.git
Enter folder "tlc/src".
Run "export SERIOUS=1; make LibList.vo" to produce the necessary vo files.
Then "time coqc -R . TLC LibList.v".
And "coqide -R . TLC LibList.v", then request compilation to the last line.
---------------
Error: To rename arguments the "rename" flag must be specified.
Argument y renamed to x.
---------------
Axiom eq_trans : forall (A:Type) (y x z:A),
x = y -> y = z -> x = z.
BEFORE
Implicit Arguments eq_trans [A].
AFTER
Arguments eq_trans [A] y x z _ _.
---------------
This command is just asserting the number and names of arguments of
eq_dep_nd. If this is what you want add ': assert' to silence the warning. If
you want to clear implicit arguments add ': clear implicits'. If you want to
clear notation scopes add ': clear scopes'
[arguments-assert,vernacular]
=> no comment
----------------
pb coexist vio & vo
----------------
In nested Ltac calls to "inverts", "libtac_invert_noregen", "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end) and "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), last call failed.
Error: No matching clauses for match.
-----------------
-async-proofs off
-async-proofs-j n
for coqide is not documented
......@@ -474,3 +474,227 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f
(*
Lemma Rule_op : forall op (n1 n2:int),
Triple ((prim_op op) (val_pair (enc n1) (enc n2))) \[] (fun r => \[r = op n1 n2]).
Proof using.
intros. applys rule_consequence. { auto. } { applys rule_op. }
{ intros r. unfold PostEnc. hsimpl~ (op n1 n2). }
Qed.
Lemma Rule_if_trm : forall t0 t1 t2 H Q0 Q,
Triple t0 H Q0 ->
(forall X, Triple (trm_if X t1 t2) (Q0 X) Q) ->
Triple (trm_if_trm t0 t1 t2) H Q.
Admitted.
Lemma Rule_seq : forall t1 t2 H Q H',
Triple t1 H (fun v => H') ->
Triple t2 H' Q ->
Triple (trm_seq t1 t2) H Q.
Admitted.
Lemma Rule_while : forall t1 t2 H Q,
(forall (k:trm),
(forall H Q, triple (trm_if_trm t1 (trm_seq t2 k) val_unit) H Q -> triple k H Q) ->
triple k H Q) ->
triple (trm_while t1 t2) H Q.
Admitted.
*)
(* LATER
Definition mlist_incr_val : val :=
Fix mlist_incr [p] :=
_If trm_app val_neq [val_var p; val_loc null] Then (
Let x := prim_get [val_var p; val_field hd] in
Let q := prim_get [val_var p; val_field tl] in
Let y := trm_app val_add [val_var x; val_int 1] in
prim_set [val_var p; val_field hd; val_var y];;
trm_app mlist_incr [val_var q]
).
(*
Lemma mlist_incr_spec : forall p L,
triple (trm_app mlist_incr_val [p])
(p ~> MList L)
(p ~> MList L)
*)
(** Functions *)
Parameter val_fun : var -> vars -> trm -> trm.
Notation "'Fun' f [ x1 ] ':=' K" :=
(val_fun f (x1:nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 ] ':=' K" :=
(val_fun f (x1::nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 ] ':=' K" :=
(val_fun f (x1::x2::nil) K)
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 ] ':=' K" :=
(val_fun f (x1::x2::x3::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 x4 ] ':=' K" :=
(val_fun f (x1::x2::x3::x4::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident) : trm_scope.
Notation "'_If' x 'Then' F1" :=
(trm_if x F1 val_unit)
(at level 69, x at level 0) : trm_scope.
Notation "x `+` y" := (trm_app val_add [x; y])
(at level 69, right associativity) : trm_scope.
Notation "r `^` f" :=
((*trm_app*) prim_get ([ r ; val_field f ]:list val))
(at level 69, no associativity, f at level 0,
format "r `^` f") : trm_scope.
Notation "r `^` f `<-` v" :=
((*trm_app*) prim_set ([r ; val_field f ; v ]:list val))
(at level 69, no associativity, f at level 0,
format "r `^` f `<-` v") : trm_scope.
(*------------------------------------------------------------------*)
(* ** Definition of the CF generator *)
Definition cf_def cf (t:Trm) :=
match t with
| Trm_val v => local (cf_val v)
| Trm_if v t1 t2 => local (cf_if v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun `{EA:Enc A} (X:A) => cf (Subst_Trm x X t2)))
| Trm_let_fix f x t1 t2 => local (cf_fix
(fun F `{EA:Enc A} (X:A) => cf (subst_Trm f F (Subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
| Trm_app f v => local (cf_app f v)
| _ => local (cf_fail)
end.
Definition cf := FixFun cf_def.
Ltac smath := simpl; math.
Hint Extern 1 (lt _ _) => smath.
Lemma cf_unfold : forall t,
cf t = cf_def cf t.
Proof using.
applys~ (FixFun_fix (measure Trm_size)). auto with wf.
intros f1 f2 t IH. unfold measure in IH. unfold cf_def.
destruct t; fequals.
{ rewrite~ IH. rewrite~ IH. }
{ rewrite~ IH. fequals.
apply func_ext_dep_3. intros A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. rewrite~ Trm_size_subst. }
{ fequals.
{ apply func_ext_dep_4. intros F A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. do 2 rewrite~ Trm_size_subst. }
{ apply func_ext_1. intros X. rewrite~ IH. rewrite~ Trm_size_subst. } }
Qed.
(********************************************************************)
(* ** Soundness proof *)
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Definition sound_for (t:trm) (F:formula) :=
forall H `{EA:Enc A} (Q:A->hprop), 'F H Q -> Triple t H Q.
(*------------------------------------------------------------------*)
(* ** Soundness of local *)
Lemma local_sound : forall t (F:formula),
sound_for t F ->
sound_for t (local F).
Admitted.
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Lemma cf_sound : forall (t:Trm),
sound_for t (cf t).
Proof using.
intros t. induction_wf: Trm_size t.
rewrite cf_unfold. destruct t; simpl;
applys local_sound; intros H A EA Q P.
{ destruct P as (V&EV&HV). applys~ Rule_val V. }
Abort.
(*------------------------------------------------------------------*)
(* ** Specialize version of [cf_fix] for small arities *)
Definition cf_fix0 (F1of : val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(F1of F ===> app F nil) ->
(F2of F) H Q.
Definition cf_fix1 (F1of : val -> val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall X1, (F1of F X1) ===> app F [X1]) ->
(F2of F) H Q.
(* LATER
Definition cf_fix2 (F1of : val -> val -> val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall X1 X2, (F1of F X1 X2) ===> app F [X1;X2]) ->
(F2of F) H Q.
*)
Lemma cf_fix_specialize_0 : forall (F1of : val -> formula) (F2of : val -> formula),
cf_fix0 F1of F2of ===>
cf_fix 0 F1of F2of
cf_fix0 (fun F => let E := List.combine (f::nil) (F::nil) in cf (subst_Trm E t1))
let G := match xs with
| nil =>
| x::nil => cf_fix1 (fun F X => let E := List.combine (f::x::nil) (F::X::nil) in cf (subst_Trm E t1))
| xs => cf_fix (List.length xs) (fun F Xs => let E := List.combine (f::xs) (F::Xs) in cf (subst_Trm E t1))
Definition cf_fix (n:nat) (F1of : val -> vals -> formula)
(F2of : val -> formula) : formula := fun H Q =>
Definition cf_fix0 (F1of : val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
......@@ -957,6 +957,7 @@ let order_record () =
(********************************************************************)
(* ** While loops *)
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
......
......@@ -87,6 +87,15 @@ let rec coqtops_of_imp_cf cf =
(* (!B: curried 2 f /\
(forall Ai x1 x2 H Q, CF H Q -> app f [(dyn t1 x1) (dyn t2 x2)] H Q) *)
| Cf_let ((x,typ), cf1, cf2) ->
let c1 = coq_of_cf cf1 in
let c2 = Coq_fun ((x, typ), coq_of_cf cf2) in
let f_core = coq_apps (coq_var "CFML.CFPrint.cf_let") [c1;c2] in
let f = Coq_app (Coq_var "CFML.CFHeaps.local", f_core) in
coq_tag "tag_let" ~label:x f
(* OLD
| Cf_let ((x,typ), cf1, cf2) ->
let q1 = Coq_var "Q1" in
let type_of_q1 = Coq_impl (typ, hprop) in
......@@ -94,6 +103,7 @@ let rec coqtops_of_imp_cf cf =
let c2 = coq_foralls [x,typ] (coq_apps (coq_of_cf cf2) [(Coq_app (q1, Coq_var x)); q]) in
funhq "tag_let" ~label:x (coq_exist "Q1" type_of_q1 (coq_conj c1 c2))
(* !L: fun H Q => exists Q1, F1 H Q1 /\ forall (x:T), F2 (Q1 x) Q *)
*)
| Cf_let_poly (x, fvs_strict, fvs_other, typ, cf1, cf2) ->
let type_of_x = coq_forall_types fvs_strict typ in
......
......@@ -631,11 +631,22 @@ Notation "'Funs' f1 ':=' K1 'and' f2 ':=' K2 'and' f3 ':=' K3 'in' F" :=
(********************************************************************)
(** Let *)
Definition cf_let (A B : Type) (F1:~~A) (F2:A->~~B) : ~~ B :=
(fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 x (Q1 x) Q).
Implicit Arguments cf_let [A B].
Notation "'Let' x ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q))
(!Let (cf_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
(* OLD
Notation "'Let' x ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q))
(at level 69, x ident, right associativity, only parsing,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
*)
Notation "'Let' x ':' T ':=' F1 'in' F2" :=
(!Let (fun H Q => exists Q1, F1 H Q1 /\ forall x:T, F2 (Q1 x) Q))
(at level 69, x ident, right associativity, only parsing) : charac.
......
......@@ -1067,39 +1067,58 @@ Qed.
Ltac xlet_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ | cont1 tt; cont2 tt ];
xtag_pre_post.
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
cont0 tt;
split; [ | cont1 x; cont2 tt ];
xtag_pre_post
end.
Ltac xlet_def cont0 cont1 cont2 :=
Ltac xlet_pre tt :=
xpull_check_not_needed tt;
xuntag tag_let;
xlet_core cont0 cont1 cont2.
xuntag tag_let.
Tactic Notation "xlet" constr(Q) "as" simple_intropattern(x) :=
Ltac xlet_def cont0 cont1 cont2 :=
xlet_pre tt; xlet_core cont0 cont1 cont2.
Ltac xlet_intros_cont x :=
let a := fresh x in intros a.
Ltac xlet_spec_as Q x :=
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intros x)
ltac:(fun _ => try xpull).
Tactic Notation "xlet" constr(Q) :=
Ltac xlet_spec Q :=
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intro)
xlet_intros_cont
ltac:(fun _ => try xpull).
Tactic Notation "xlet" "as" simple_intropattern(x) :=
Ltac xlet_as x :=
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intros x)
ltac:(fun _ => idtac).
Tactic Notation "xlet" :=
Ltac xlet_basic tt :=
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intro)
xlet_intros_cont
ltac:(fun _ => idtac).
Tactic Notation "xlet" constr(Q) "as" simple_intropattern(x) :=
xlet_spec_as Q x.
Tactic Notation "xlet" constr(Q) :=
xlet_spec Q.
Tactic Notation "xlet" "as" simple_intropattern(x) :=
xlet_as x.
Tactic Notation "xlet" :=