Commit 7232de3d authored by POTTIER Francois's avatar POTTIER Francois
Browse files
parents e9e425c1 38d59aeb
.PHONY: all tools coqlib ocamllib quick doc clean
.PHONY: all tools coqlib stdlib quick doc clean
###############################################################################
#
......@@ -21,9 +21,9 @@ TOOLS := $(CFML)/lib/tools
###############################################################################
# Targets
all: ocamllib coqlib
all: stdlib coqlib
quick: ocamllib coqlib_quick
quick: stdlib_quick coqlib_quick
coqlib:
$(MAKE) -C lib/coq proof
......@@ -31,12 +31,20 @@ coqlib:
coqlib_quick:
$(MAKE) -C lib/coq quick
ocamllib: tools
$(MAKE) -C lib/ocaml
# quick_cf builds what is needed for compiling characteristic formulae files (CFHeader)
coqlib_quick_cf:
$(MAKE) -C lib/coq quick_cf
stdlib: tools coqlib
$(MAKE) -C lib/stdlib
stdlib_quick: tools coqlib_quick
$(MAKE) -C lib/stdlib quick
demos: all
$(MAKE) -C examples
###############################################################################
# Tools
......@@ -46,19 +54,20 @@ tools:
ln -sf $(CFML)/generator/makecmj.native $(TOOLS)/cfml_cmj
ln -sf $(CFML)/generator/myocamldep.native $(TOOLS)/cfml_dep
###############################################################################
# Clean
clean_gen:
$(MAKE) -C generator clean
clean_ocamllib:
$(MAKE) -C lib/ocaml clean
clean_stdlib:
$(MAKE) -C lib/stdlib clean
clean_coqlib:
$(MAKE) -C lib/coq clean
clean: clean_gen clean_ocamllib clean_coqlib
clean: clean_gen clean_stdlib clean_coqlib
###############################################################################
......
-- xfor_inv prefers to use b-1 as upper bound if possible
(* todo: warning if not the right nb of args on xapp *)
-- xapp as b'
-- xapp on a leaf does not do xpull
-> corriger let n = null qui ne génère pas ce qu'il faut
- xfor_inv tag goal
-- case_if checking single goal
unifier main.ml et makecmj.ml
-- xmatch_no_intros should do the inversion.
se débarrasser de myocamldep serait agréable
-- improve xauto spec
NullPointers et StrongPointers sont spéciaux puisque l'utilisateur
va devoir lier son code OCaml avec eux; ils ne devraient pas être
installés avec la lib standard?
-- xcf_show without argument should put at head of goal
-- xunfold at fait pas le unfold
-- Ouvrir liblistZ à la fin de cflib
-- Demo de la notation pour les records
-- Array : compléter.
-- LibListZ.sub
-- Array.iter forall l, Array xs \c I l
-- renommer Array.of_list
-- utiliser "of_list []" à la place de make_empty
-- régler le "==>"
-- 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
- xclose with args for the change.
(* 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.
*)
- xsimpl on I X ==> I Y produces X = Y.
- xapp_rm
- generate inhab instance for algebraic
- xwhile needs to call tag_pre_post in branches
- hint spec based on type args
- xchanges
- implement xpush.
- xwhile: error reporting when arguments don't have the right types.
MAJOR TODAY
MAJOR NEXT
- record with imperative
- partial/over application
- "xapp as x" pratique sur xlet
"xapps as x" pratique sur xlet
- Sys.max_array_length discuss with francois
- patterns and when clauses
- add support for pure records
Record 'A T := T_intro { f' : T1; .. }
if mutually recursive, encode record def using
Ind 'A T := T_intro : T1 -> ... -> 'A T
Implicit Types T ['A]
Def f' 'A (p:'A T) :=
match p with T_intro x1 .. xN => xi end
alloc: (T_intro v1 .. vN : typ)
set : impossible
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
let H := cfml_get_precondition tt in
xlet (... \*+ H)
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
t ~> Array L= t ~> Arraylen n * exists G, Groupof Cell G
dom G = [0,n] * lenght L = n * forall i indom G, L[i] = G[i]
- realize array specification using single-cell array specifications
- see if we can get rid of make_cmj, using -only-cmj
=> make_cmj seems to already be never used.
MAJOR POSTPONED
- support char, string, float
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
- would it be better to perform all renaming during normalization phase?
- have a flag to control whether functions such as "min", "max", "abs", etc..
should be systematically let-bound; this would allow binding these names.
- mutual recursive definitions, polymophic type variables should be more precise
##################################################################
# FUTURE WORK
OTHER LANGUAGES
- semantics for records|arrays passed by value / passed by reference
- support null pointers
CODE BEAUTIFY
- better error message when calling [xapp] on a record application
in which the record is not unfocused.
- make sure that check_var is called where needed
- unify the source code in main.ml and makecmj.ml
- check that there are no uses of labels in input source files
- Ltac xcf_core tt
should be able to test whether Spec is a top val, and then do rewrite.
MAKEFILE BEAUTIFY
- no longer rely on myocamldep
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- In the makefile.Coq, when building the .vq and obtaining
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
=> then delete the .vio file
(useful for compilations interrupted using CTRL+C)
=> even better, wrap "coqc -quick" with an atomic commit of its result.
##################################################################
# PROPOSAL FOR DEFENSIVE CODE
- VStack.ml contains a verified stack implemementation using CFML.
(not polluted by any runtime checks).
- SStack.ml is a wrapper for VStack which adds asserts;
e.g. let pop s = assert (!s <> nil); VStack.pop s
- The file SStack.ml is processed using a special mode of CFML,
in which "assert t" is interpreted as "t needs to run safely
and produce some boolean; and the rest of the code may
assume this boolean to be true". Formally:
(Assert F) H Q :=
exists (P:Prop),
(F H (fun (b:bool) => [b = true <-> P] \* H))
/\ (H \* [P] ==> Q tt)
During the proof, the user needs to provide the proposition
[P] that is tested by the assertion. This proposition can
be assumed to be true after the assert is executed.
##################################################################
# COQ BUG
-async-proofs off
-async-proofs-j n
for coqide is not documented
omega requires Z.sub to be transparent, but this is an issue for simpl.
Set Implicit Arguments.
Require Export LibInt CFApp CFPrint.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* DEPRECATED
(*-- version very old *)
Notation "'While' Q1 'Do' Q2 '_Done'" :=
(!While (fun H Q => forall R:~~unit, is_local R ->
(forall H Q, (If_ Q1 Then (Q2 ;; R) Else (Ret tt)) H Q -> R H Q)
-> R H Q))
(at level 69, Q2 at level 68, only parsing) : charac.
Lemma while_loop_cf_to_inv' :
forall (A:Type) (I:A->hprop) (J:A->bool->hprop) (lt:binary A),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
wf lt ->
(exists X0, H ==> (I X0)) ->
(forall X, F1 (I X) (J X)
/\ F2 (J X true) (# Hexists Y, (I Y) \* \[lt Y X])
/\ J X false ==> Q tt) ->
(While F1 Do F2 _Done) H Q.
Proof.
introv W (X0&I0) M. apply local_erase.
introv LR HR. applys* local_weaken (rm I0). gen X0.
intros X. induction_wf IH: W X.
destruct (M X) as (M1&M2&M3).
applys HR. xlet*. xif. xseq*. xextract as Y L.
xapply* IH; hsimpl.
xret_no_gc~.
Qed.
Lemma while_loop_cf_to_inv :
forall (A:Type) (I:A->hprop) (B:A->bool->Prop) (lt:binary A) (W:wf lt),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists X0, H ==> (I X0)) ->
(forall X, F1 (I X) (fun b => \[B X b] \* I X)
/\ F2 (\[B X true] \* I X) (# Hexists Y, (I Y) \* \[lt Y X])
/\ \[B X false] \* I X ==> Q tt) ->
(While F1 Do F2 _Done) H Q.
Proof.
intros. eapply while_loop_cf_to_inv' with (J:= fun X b => \[B X b] \* I X); eauto.
Qed.
Ltac xwhile_inv_core W I B :=
match type of W with
| wf _ => eapply (@while_loop_cf_to_inv _ I B _ W)
| _ -> nat => eapply (@while_loop_cf_to_inv _ I B (measure W)); [ try prove_wf | | ]
| _ => eapply (@while_loop_cf_to_inv _ I B W); [ try prove_wf | | ]
end.
Tactic Notation "xwhile_inv" constr(W) constr(I) constr(B) :=
xwhile_pre ltac:(fun _ => xwhile_inv_core W I B).
Tactic Notation "xwhile_inv_body" :=
apply local_erase; esplit; splits (3%nat).
(*-- version old *)
(** [xwhile_inv I] proves a while loop using an invariant of the
form [fun b m => H], where [b] is a boolean value that describes
whether the loop condition returns true, and where [m] is an
integer whose value should decrease towards zero at every iteration. *)
Lemma while_loop_cf_inv_measure :
forall (I:bool->int->hprop),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists b m, H ==> I b m) ->
(forall b m, F1 (I b m) (fun b' => Hexists m', I b' m')) ->
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(forall m, I false m ==> Q tt \* Hexists H', H') ->
(While F1 Do F2 _Done) H Q.
(* TODO: see cf spec *)
Ltac xwhile_inv_measure_core I :=
apply (@while_loop_cf_inv_measure I).
Tactic Notation "xwhile_inv" constr(I) :=
xwhile_pre ltac:(fun _ => xwhile_inv_measure_core I).
(*--version was in this file *)
Definition while_loop_cf (F1:~~bool) (F2:~~unit) :=
local (fun (H:hprop) (Q:unit->hprop) => forall R:~~unit, is_local R ->
(forall H Q, (exists Q', F1 H Q'
/\ (local (fun H Q => exists Q', F2 H Q' /\ R (Q' tt) Q) (Q' true) Q)
/\ Q' false ==> Q tt) -> R H Q)
-> R H Q).
Definition while_loop_inv (F1:~~bool) (F2:~~unit) :=
local (fun (H:hprop) (Q:unit->hprop) =>
exists (A:Type) (I:A->hprop) (J:A->bool->hprop) (lt:binary A),
wf lt
/\ (exists X0, H ==> (I X0))
/\ (forall X, F1 (I X) (J X)
/\ F2 (J X true) (# Hexists Y, (I Y) \* \[lt Y X])
/\ J X false ==> Q tt)).
Lemma while_loop_cf_to_inv : forall (F1:~~bool) (F2:~~unit),
while_loop_inv F1 F2 ===> while_loop_cf F1 F2.
Proof using.
intros. apply local_weaken_body. intros H Q (A&I&J&lt&W&(X0&I0)&M).
introv LR HR. applys* local_weaken I0. clear I0. gen X0.
intros X. induction_wf IH: W X.
destruct (M X) as (M1&M2&M3).
applys HR. exists (J X). splits~.
apply local_erase. esplit. split. apply M2.
applys local_extract_exists; autos~. intros x.
rewrite star_comm. apply~ local_intro_prop.
Qed.
Lemma while_loop_cf_inv_measure :
forall (I:bool->int->hprop),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists b m, H ==> I b m) ->
(forall b m, F1 (I b m) (fun b' => I b' m)) ->
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(forall m, I false m ==> Q tt \* Hexists H', H') ->
while_loop_cf F1 F2 H Q.
Proof using.
introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc (I bi mi). xlocal.
clear Hi. apply local_erase. introv LR HR.
gen bi. induction_wf IH: (int_downto_wf 0) mi. intros.
applys (rm HR). esplit. splits.
applys Hc.
simpl. apply local_erase. esplit. split.
applys Hs.
simpl. eapply local_extract_exists. xlocal. intros b.
eapply local_extract_exists. xlocal. intros m'.
eapply local_intro_prop with (F:=R). auto. intros E.
applys IH. applys E.
simpl. applys He.
Qed.
Definition for_loop_cf (a:int) (b:int) (F:~~unit) :=
local (fun (H:hprop) (Q:unit->hprop) => forall S:int->~~unit, is_local_pred S ->
(forall i H Q,
((i <= (b)%Z -> (local (fun H Q => exists Q', F H Q' /\ S (i+1) (Q' tt) Q) H Q))
/\ (i > b%Z -> H ==> Q tt))
-> S i H Q)
-> S a H Q).
Definition for_loop_inv (a:int) (b:int) (F:~~unit) :=
local (fun (H:hprop) (Q:unit->hprop) =>
(a > (b)%Z -> H ==> (Q tt))
/\ (a <= (b)%Z -> exists H', exists I,
(H ==> I a \* H')
/\ (forall i, a <= i /\ i <= (b)%Z -> F (I i) (# I(i+1)))
/\ (I ((b)%Z+1) \* H' ==> Q tt))).
Lemma for_loop_cf_to_inv : forall (a:int) (b:int) (F:~~unit),
for_loop_inv a b F ===> for_loop_cf a b F.
Proof using.
intros. apply local_weaken_body. intros H Q (Mgt&Mle). introv LS HS.
tests C: (a > b). apply HS. split. math. auto.
clear Mgt. specializes Mle. math. destruct Mle as (H'&I&M1&M2&M3).
applys~ (@local_wframe unit) (# I (b+1)); [| intros u; destruct~ u ].
clear M1. asserts L: (a <= a <= b+1). math. generalize L.
set (a' := a) at 1. generalize a as i. unfold a'.
intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd.
applys HS. split; intros C'.
apply local_erase. esplit. split.
apply M2; auto with maths.
forwards: IH (i+1); auto with maths.
math_rewrite~ (i = b +1).
Qed.
*)
(************************************************************)
(* ** [xgo] *)
Inductive Xhint_cmd :=
| Xstop : Xhint_cmd
| XstopNoclear : Xhint_cmd
| XstopAfter : Xhint_cmd
| XstopInside : Xhint_cmd
| Xtactic : Xhint_cmd
| XtacticNostop : Xhint_cmd
| XtacticNoclear : Xhint_cmd
| XsubstAlias : Xhint_cmd
| XspecArgs : list Boxer -> list Boxer -> Xhint_cmd
| Xargs : forall A, A -> Xhint_cmd
| Xlet : forall A, A -> Xhint_cmd
| Xlets : forall A, A -> Xhint_cmd
| Xsimple : Xhint_cmd.
Inductive Xhint (a : tag_name) (h : Xhint_cmd) :=
| Xhint_intro : Xhint a h.
Ltac add_hint a h :=
let H := fresh "Hint" in
lets H: (Xhint_intro a h).
Ltac clear_hint a :=
match goal with H: Xhint a _ |- _ => clear H end.
Ltac clears_hint tt :=
repeat match goal with H: Xhint _ _ |- _ => clear H end.
Ltac find_hint a :=
match goal with H: Xhint a ?h |- _ => constr:(h) end.
Ltac xgo_default solver cont :=
match ltac_get_tag tt with
| tag_ret => xret; cont tt
| tag_fail => xfail; cont tt
| tag_done => xdone; cont tt
| tag_apply => xapp
| tag_seq => xseq; cont tt
| tag_let_val => xval; cont tt
| tag_let_trm => xlet; cont tt
| tag_let_fun => fail
| tag_body => fail
| tag_letrec => fail
| tag_case => xcases_real; cont tt
| tag_casewhen => fail
| tag_if => xif; cont tt
| tag_alias => xalias; cont tt
| tag_match ?n => xmatch; cont tt
| tag_top_val => fail
| tag_top_trm => fail
| tag_top_fun => fail
| tag_for => fail
| tag_while => fail
end.
Ltac xtactic tag := idtac.
Ltac run_hint h cont :=
let tag := ltac_get_tag tt in
match h with
| Xstop => clears_hint tt; idtac
| XstopNoclear => idtac
| XstopAfter =>
match tag with
| tag_let_trm => fail (* todo: xlet_with cont ltac:(fun _ => idtac)*)
| _ => xgo_default ltac:(fun _ => idtac) ltac:(fun _ => idtac)
end
| XstopInside =>
match tag with
| tag_let_trm => fail (*todo: xlet_with ltac:(fun _ => idtac) cont *)
end
| Xtactic => clears_hint tt; xtactic tag
| XtacticNostop => xtactic tag; cont tt
| XtacticNoclear => xtactic tag
| XsubstAlias => xmatch_subst_alias; cont tt
| Xargs ?E =>
match tag with
| tag_let_trm => fail (* todo!!*)
| tag_apply => xapp E (*todo: not needed?*)
end
| XspecArgs (>> ?S) ?E =>
match tag with
| tag_let_trm => fail (* todo!!*)
| tag_apply => xapp_spec S E (*todo: not needed?*)
end
| Xlet ?S =>
match tag with
| tag_let_trm => xlet S; cont tt
| tag_let_fun => xfun_noxbody S
end
| Xsimple => xmatch_simple; cont tt
(* todo : generalize
| tag_case => xcases_real
| tag_if => xif
| tag_match ?n => xmatch
*)
end.
Ltac find_and_run_hint cont :=
let a := ltac_get_label tt in
let h := find_hint a in
clear_hint a;
first [ run_hint h cont | fail 1 ].
Tactic Notation "xhint" :=
find_and_run_hint ltac:(fun _ => idtac).
Ltac xgo_core solver cont :=
first [ find_and_run_hint cont
| xgo_default solver cont ].
Ltac xgo_core_once solver :=
xgo_core solver ltac:(fun _ => idtac).
Ltac xgo_core_repeat solver :=
xgo_core solver ltac:(fun _ => instantiate; try solve [ solver tt ];
instantiate; try xgo_core_repeat solver).
Ltac xgo_pre tt :=
first [ xcf; repeat progress(intros)
| repeat progress(intros)
| idtac ].
Ltac xgo_base solver :=
xgo_pre tt; xgo_core_repeat solver.
Tactic Notation "xgo1" :=
xgo_core_once ltac:(fun _ => idtac).
Tactic Notation "xgo" :=
xgo_base ltac:(fun tt => idtac).
Tactic Notation "xgo" "~" :=