Commit 52584dfc authored by charguer's avatar charguer

stable

parent c4e908e4
......@@ -7,7 +7,6 @@ Open Scope tag_scope.
(********************************************************************)
(********************************************************************)
......@@ -565,16 +564,16 @@ Proof using.
{ dup 10.
{ xors. xapps. xsimpl~. subst. xclean. xauto*. }
{ xors \[=true]. xapps. xsimpl~. skip. }
{ xor \[=true]. xapps. xsimpl. skip. }
{ xor \[=true]. hsimpl. xapps. xsimpl. skip. }
{ xif_no_simpl. skip. skip. }
{ xpost. xif_no_simpl \[= true]. skip. skip. skip. }
{ xpost. xif_no_simpl \[=true] as R.
{ xclean. false. }
{ xapps. xsimpl. subst. xclean. xauto*. }
xsimpl~. }
{ xpost. xif_no_intros \[=true]. intros R. skip. skip. }
{ xpost. xif_no_intros \[=true]. intros R. skip. skip. skip. }
{ xpost. xif_no_simpl_no_intros \[=true]. intros R. skip. skip. skip. }
{ xif. xapps. xsimpl. skip. }
{ xif. xrets. xapps. xsimpl. skip. }
{ xgo*. subst. xclean. auto. }
(* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
}
......@@ -590,7 +589,7 @@ Proof using.
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets*. }
xlet \[= true].
{ xif. xapps. xors. xapps. xrets. extens. rew_refl. autos*. }
{ xif. xapps. xors. xapps. xrets. autos*. }
{ intro_subst. xif. xrets~. }
Qed.
......@@ -605,11 +604,11 @@ Lemma compare_poly_spec :
Proof using.
xcf.
xlet_poly_keep (= true).
{ xapps. xpolymorphic_eq. xsimpl. subst r. logics~. }
{ xapps. xpolymorphic_eq. xsimpl. subst r. rew_bool_eq~. }
intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xlet_poly_keep (= true).
{ xapps. xpolymorphic_eq. xsimpl. subst r. logics~. }
{ xapps. xpolymorphic_eq. xsimpl. subst r. rew_bool_eq~. }
intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xrets~.
......@@ -660,7 +659,7 @@ Proof using.
{ xmatch.
{ xrets~. }
{ xapps~. xrets. xif.
{ xrets. case_if. auto. }
{ xrets. cases_if. auto. }
{ xapp_spec infix_emark_eq_gen_spec. intros M. xif.
{ xrets. case_if~. }
{ xrets. case_if~. rewrite~ M. } } } }
......@@ -1400,7 +1399,7 @@ Lemma Sitems_close : forall r A (L:list A) (n:int),
r ~> Sitems L.
Proof using. intros. xunfolds~ Sitems. Qed.
Implicit Arguments Sitems_close [].
Arguments Sitems_close : clear implicits.
(* TODO comment
r ~> Sitems _
xopen r
......@@ -1429,7 +1428,7 @@ Require Import Array_proof TLC.LibListZ.
Section Array.
Hint Extern 1 (@index _ (list _) _ _ _) => apply index_bounds_impl : maths.
Hint Extern 1 (@index _ (list _) _ _ _) => apply index_of_inbound : maths.
Hint Extern 1 (_ < length (?l[?i:=?v])) => rewrite length_update : maths.
Ltac auto_tilde ::= auto with maths.
......@@ -1440,12 +1439,12 @@ Proof using.
xapp. math. => L EL.
asserts LL: (LibListZ.length L = 3).
{ subst. rewrite LibListZ.length_make; math. }
xapps. { apply index_bounds_impl; math. }
xapps. { apply index_of_inbound; math. }
xapp~.
xapps~.
xapps~.
xapps~.
xsimpl. subst. rew_arr~.
xsimpl. subst. rew_array~.
Qed.
End Array.
......
EXAMPLE_DIRS = \
Demos \
Tuto \
BinaryRandomAccessList \
Tuto
#\ BinaryRandomAccessList \
# TO FIX:
# BatchedQueue => OCaml complains about ungeneralized type variable (!?)
......
##############################################################################
#
# This Makefile can be used to compile examples, including the recompilation
# of all dependencies. Only for developper use.
#
# In an example folder, type
# make -f ../Makefile.dev
#
##############################################################################
# CFML setup.
CFML := $(shell cd ../.. && pwd)
include $(CFML)/Makefile.common
##############################################################################
# Compilation.
PWD := $(shell pwd)
export
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R $(CFML)/lib/stdlib CFML.Stdlib \
-R $(PWD) EXAMPLE
##############################################################################
# Files.
PWD := $(shell pwd)
LIBCOQ := $(CFML)/lib/coq
STDLIB := $(CFML)/lib/stdlib
STDLIB_ML := $(wildcard $(STDLIB)/*.ml)
STDLIB_CMJ := $(patsubst %.ml,%.cmj,$(STDLIB_ML))
ifndef ML
ML := $(wildcard $(PWD)/*.ml)
endif
CMJ := $(patsubst %.ml,%.cmj,$(ML))
ifndef V
V := $(patsubst %.ml,%_ml.v,$(ML)) \
$(patsubst %.ml,%_proof.v,$(ML))
endif
V_AUX_BASE := $(wildcard $(LIBCOQ)/*.v) \
$(wildcard $(STDLIB)/*.v)
ifdef INCLUDE_TLC_AS_DEPENDENCIES
# encompass TLC in the scope of the dependency graph.
# This allows us to recompile part of TLC, if it has changed.
V_AUX := $(wildcard $(TLC)/*.v) \
$(V_AUX_BASE)
else
V_AUX := $(V_AUX_BASE)
endif
##############################################################################
# Targets.
.PHONY: all
all: $(CMJ)
# Must run in two successive phases, as coqdep must not run until the
# files %_ml.v have been generated. So, we create the files %.cmj and
# %_ml.v first (above), then compile every .v file.
@ $(MAKE) -f $(TLC)/Makefile.coq $@
_CoqProject:
@ $(MAKE) -f $(TLC)/Makefile.coq $@
##############################################################################
# Generating %.cmj and %_ml.v.
CFML_FLAGS :=
# can use:
# -only_cmj
# and OCaml flags
# Note: we must delete the .cmj file if the construction of the _ml.v file
# has failed. (Maybe the generator itself should take care of that!)
# Note: at the moment, we do not run ocamldep, and assume that there no
# inter-module dependencies. Every module is allowed to implicitly depend
# on Pervasives.
ifndef CFMLC
CFMLC=$(CFML)/generator/main.native
endif
$(STDLIB)/Pervasives_ml.v $(STDLIB)/Pervasives.cmj: $(STDLIB)/Pervasives.ml $(CFMLC)
$(CFMLC) $(CFML_FLAGS) -nostdlib -nopervasives -I $(STDLIB) $< || (rm -f $@; exit 1)
$(STDLIB)/%_ml.v $(STDLIB)/%.cmj: $(STDLIB)/%.ml $(STDLIB)/Pervasives.cmj $(CFMLC)
$(CFMLC) $(CFML_FLAGS) -nostdlib -I $(STDLIB) $< || (rm -f $@; exit 1)
$(PWD)/%_ml.v $(PWD)/%.cmj: $(PWD)/%.ml $(STDLIB_CMJ) $(CFMLC)
$(CFMLC) $(CFML_FLAGS) -I $(STDLIB) -I . $< || (rm -f $@; exit 1)
##############################################################################
# Cleanup.
clean::
rm -rf *.cmj *_ml.v _output
@ $(MAKE) -f $(TLC)/Makefile.coq $@
......@@ -32,6 +32,7 @@ export
TLC := $(shell $(COQBIN)coqc -where)/user-contrib/TLC
##############################################################################
# Options for CFML.
......
......@@ -87,9 +87,9 @@ Parameter not_divide_prime_sqrt : forall n r,
Ltac auto_tilde ::= try solve [ intuition eauto with maths ].
Hint Extern 1 (index ?M _) => subst M : maths.
Hint Resolve index_zmake : maths.
Hint Resolve index_bounds_impl : maths.
Hint Resolve index_length_unfold int_index_prove : maths.
Hint Resolve LibListZ.index_make : maths.
Hint Resolve index_of_inbound : maths.
Hint Resolve index_of_index_length int_index_prove : maths.
Hint Resolve index_update : maths.
(** Tactic [rew_maths] for simplifying math expressions *)
......@@ -436,6 +436,9 @@ let is_prime n =
!p
----*)
Require Import Psatz.
Tactic Notation "math_nia" := math_setup; nia.
Lemma is_prime_spec : forall n,
n >= 2 ->
app is_prime [n]
......@@ -468,7 +471,7 @@ Proof using.
{ eauto. }
{ math_nia. } }
=> k vp Hb Hvp Hk. xclean. rew_logic in Hb.
xapps. xsimpl. subst. case_if.
xapps. xsimpl. subst. case_if; rew_bool_eq.
{ destruct Hb; tryfalse. applys* not_divide_prime_sqrt. math. }
{ auto. }
Qed.
......@@ -584,7 +587,7 @@ Definition Stack A (L:list A) r :=
r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
Implicit Arguments Stack_close [].
Arguments Stack_close : clear implicits.
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
......
......@@ -353,7 +353,8 @@ let inductive_lhs rhs r =
(* An implicit argument specification. *)
let implicit (x, i) =
(* DEPRECATED
let deprecated_implicit (x, i) =
match i with
| Coqi_maximal ->
brackets (string x)
......@@ -361,6 +362,16 @@ let implicit (x, i) =
string x
| Coqi_explicit ->
sprintf "(* %s *)" x
*)
let implicit (x, i) =
match i with
| Coqi_maximal ->
braces (string x)
| Coqi_implicit ->
brackets (string x)
| Coqi_explicit ->
string x
(* -------------------------------------------------------------------------- *)
......@@ -396,10 +407,19 @@ let top = function
| Coqtop_label (x, n) ->
sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope."
x (value_variable n)
(* DEPRECATED
| Coqtop_implicit (x, xs) ->
string "Implicit Arguments " ^^
string x ^/^
brackets (flow_map space implicit xs)
brackets (flow_map space deprecated_implicit xs)
^^ dot
*)
| Coqtop_implicit (x, xs) ->
string "Arguments " ^^
string x ^/^
(if xs = []
then string ": clear implicits"
else (flow_map space implicit xs))
^^ dot
| Coqtop_register (db, x, v) ->
sprintf "Hint Extern 1 (Register %s %s) => CFHeader_Provide %s." db x v
......
......@@ -354,7 +354,7 @@ let inlined_primitives_table =
"List.length", (Primitive_unary, "(@TLC.LibListZ.length _)");
"List.rev", (Primitive_unary, "(@TLC.LibList.rev _)");
"List.concat", (Primitive_unary, "(@TLC.LibList.concat _)");
"List.append", (Primitive_binary, "(@TLC.LibList.append _)");
"List.append", (Primitive_binary, "(@TLC.LibList.app _)");
]
......
......@@ -1811,16 +1811,15 @@ Tactic Notation "xassert" :=
- [xif_no_simpl_no_intros Q']
*)
Ltac xif_post H := (* todo: cleanup *)
Ltac xif_post H := (* todo: cleanup and simplify *)
calc_partial_eq tt;
try rew_isTrue in H; (* try fold_bool; fold_prop; TODO: check change*)
try fix_bool_of_known tt;
try solve [ discriminate | false; congruence ];
first [ subst_hyp H; try rew_isTrue in H (* TODO: try fold_bool *)
first [ subst_hyp H; rew_bool_eq
| idtac ];
try fix_bool_of_known tt;
try (check_noevar_hyp H; rew_istrue in H; rew_logic in H).
try (check_noevar_hyp H; rew_bool_eq in H; rew_logic in H).
(* DEPRECATED
......
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