Commit 720c403b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into new_system

Conflicts:
	examples/in_progress/koda_ruskey.mlw
	src/parser/typing.ml
	src/transform/eval_match.ml
parents b422dcfc 28b7a239
François Bobot <francois@bobot.eu> <bobot@lri.fr>
François Bobot <francois@bobot.eu> <francois.bobot@cea.fr>
Martin Clochard <martin.clochard@lri.fr> <martin@pc-stagiaire.(none)>
Martin Clochard <martin.clochard@lri.fr> <clochard@MC-MacBook.(none)>
Sylvain Dailler <dailler@adacore.com> <sdailler@hauzar@adacore.com>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <Jean-Christophe.Filliatre@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@gemini.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@balrog.(none)>
Clément Fumex <clement.fumex@inria.fr> <fumex@moloch.lri.fr>
Léon Gondelman <gondelmans@lri.fr> <gondelmans@lri.fr>
Léon Gondelman <gondelmans@lri.fr> <lgondelmann@gmail.com>
Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
David Hauzar <david.hauzar@inria.fr> <hauzar@moloch.lri.fr>
Johannes Kanig <kanig@adacore.com> <johannes.kanig@lri.fr>
Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
Mário José Parreira Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário José Parreira Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário José Parreira Pereira <mpereira@lri.fr> <mpereira@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@atafat-desktop.(none)>
Piotr Trojanek <piotr.trojanek@altran.com> <piotr.trojanek@gmail.com>
......@@ -127,8 +127,6 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TARGET_EMACS = share/emacs/why3.elc
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
###############
......@@ -288,11 +286,7 @@ clean_old_install::
rm -rf $(OCAMLINSTALLLIB)/why3
ifeq ($(EMACS),no)
install_no_local:: clean_old_install
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
$(MKDIR_P) $(BINDIR)
$(MKDIR_P) $(LIBDIR)/why3
$(MKDIR_P) $(TOOLDIR)
......@@ -303,7 +297,6 @@ endif
$(MKDIR_P) $(DATADIR)/why3/theories
$(MKDIR_P) $(DATADIR)/why3/modules/mach
$(MKDIR_P) $(DATADIR)/why3/drivers
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
......@@ -353,16 +346,19 @@ uninstall: clean_old_install
clean_old_install::
rm -f $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
rm -f $(DATADIR)/emacs/site-lisp/why3.elc
endif
install_no_local::
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
ifeq (@enable_emacs_compilation@,yes)
$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
endif
ifeq (@enable_emacs_compilation@,yes)
all: share/emacs/why3.elc
endif
##################
# Why3 plugins
......@@ -585,7 +581,7 @@ CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES)))
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
byte opt: $(TOOLS)
all: $(TOOLS)
lib/why3server$(EXE): $(SERVER_O)
$(CC) -Wall -o $@ $^
......@@ -593,11 +589,8 @@ lib/why3server$(EXE): $(SERVER_O)
lib/why3cpulimit$(EXE): $(CPULIM_O)
$(CC) -Wall -o $@ $^
%.o: %.c %.h
$(CC) -c -Wall -g -o $@ $<
%.o: %.c
$(CC) -c -Wall -g -o $@ $<
$(CC) -Wall -O -g -o $@ -c $<
install_no_local::
$(MKDIR_P) $(LIBDIR)/why3
......@@ -1037,9 +1030,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
opt byte: $(COQVO)
install_local:: $(COQVO) drivers/coq-realizations.aux
all: $(COQVO)
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
......@@ -1062,11 +1053,11 @@ drivers/coq-realizations.aux: Makefile
endif
all: drivers/coq-realizations.aux
install_no_local::
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
opt byte: drivers/coq-realizations.aux
clean::
rm -f drivers/coq-realizations.aux
......@@ -1124,8 +1115,6 @@ install_no_local::
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
......@@ -1144,7 +1133,7 @@ install_no_local::
endif
opt byte: drivers/pvs-realizations.aux
all: drivers/pvs-realizations.aux
clean::
rm -f drivers/pvs-realizations.aux
......@@ -1293,7 +1282,7 @@ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.au
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
# all: update-isabelle
clean::
rm -f lib/isabelle/*/*.xml
......@@ -1309,7 +1298,7 @@ install_no_local::
endif
opt byte: drivers/isabelle-realizations.aux
all: drivers/isabelle-realizations.aux
clean::
rm -f drivers/isabelle-realizations.aux
......@@ -2034,7 +2023,7 @@ doc/version.tex: doc/version.tex.in config.status
config.status: configure
./config.status --recheck
opt byte: lib/why3/META .merlin
all: lib/why3/META .merlin
lib/why3/META: lib/why3/META.in config.status
./config.status chmod --file $@
......
......@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling,
AS_HELP_STRING([--enable-profiling], [enable profiling]),,
enable_profiling=no)
# Emacs compilation
AC_ARG_ENABLE(emacs-compilation,
AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
enable_emacs_compilation=yes)
# either relocation or local, not both
if test "$enable_relocation" = yes ; then
if test "$enable_local" = yes ; then
......@@ -348,7 +354,13 @@ if test "$enable_html_doc" = yes ; then
fi
# checking for emacs
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$enable_emacs_compilation" = yes ; then
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$EMACS" = no ; then
enable_emacs_compilation=no
AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
fi
fi
# checking for Zarith
if test "$enable_zarith" = yes; then
......@@ -787,6 +799,8 @@ AC_SUBST(enable_html_doc)
AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)
AC_SUBST(enable_emacs_compilation)
AC_SUBST(EMACS)
AC_SUBST(enable_frama_c)
......
......@@ -7,4 +7,5 @@ theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
end
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="60" steplimit="0" memlimit="1000"/>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......
module Bug
type foo = { a: unit -> unit ; b : unit }
constant bar : foo = {
a = fun _ -> () ;
b = ()
}
end
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../floats.why" expanded="true">
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.1.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
......
(** {1 Euler Project, problem11}
In the 20×20 grid below, four numbers along a diagonal line have been marked in red.
{h <Pre>
08 02 22 97 38 15 00 40 00 75 04 05 07 78 52 12 50 77 91 08
49 49 99 40 17 81 18 57 60 87 17 40 98 43 69 48 04 56 62 00
81 49 31 73 55 79 14 29 93 71 40 67 53 88 30 03 49 13 36 65
52 70 95 23 04 60 11 42 69 24 68 56 01 32 56 71 37 02 36 91
22 31 16 71 51 67 63 89 41 92 36 54 22 40 40 28 66 33 13 80
24 47 32 60 99 03 45 02 44 75 33 53 78 36 84 20 35 17 12 50
32 98 81 28 64 23 67 10 26 38 40 67 59 54 70 66 18 38 64 70
67 26 20 68 02 62 12 20 95 63 94 39 63 08 40 91 66 49 94 21
24 55 58 05 66 73 99 26 97 17 78 78 96 83 14 88 34 89 63 72
21 36 23 09 75 00 76 44 20 45 35 14 00 61 33 97 34 31 33 95
78 17 53 28 22 75 31 67 15 94 03 80 04 62 16 14 09 53 56 92
16 39 05 42 96 35 31 47 55 58 88 24 00 17 54 24 36 29 85 57
86 56 00 48 35 71 89 07 05 44 44 37 44 60 21 58 51 54 17 58
19 80 81 68 05 94 47 69 28 73 92 13 86 52 17 77 04 89 55 40
04 52 08 83 97 35 99 16 07 97 57 32 16 26 26 79 33 27 98 66
88 36 68 87 57 62 20 72 03 46 33 67 46 55 12 32 63 93 53 69
04 42 16 73 38 25 39 11 24 94 72 18 08 46 29 32 40 62 76 36
20 69 36 41 72 30 23 88 34 62 99 69 82 67 59 85 74 04 36 16
20 73 35 29 78 31 90 01 74 31 49 71 48 86 81 16 23 57 05 54
01 70 54 71 83 51 54 69 16 92 33 48 61 43 52 01 89 19 67 48
</Pre> }
The product of these numbers is 26 × 63 × 78 × 14 = 1788696.
What is the greatest product of four adjacent numbers in the same direction (up, down, left, right, or diagonally) in the 20×20 grid?
*)
module ProductFour
use import int.Int
use import ref.Ref
use import matrix.Matrix
use import option.Option
(** Direction of the product checked *)
type direction =
| Left_bottom
| Right_bottom
| Bottom
| Right
(* FIXME
(** Math functions about the result of a product. Incomplete product generate None *)
function left_diag (m: matrix int) (i: int) (j: int) : option int =
if (i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3) then
Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3))))
else
None
function right_diag (m: matrix int) (i: int) (j: int) : option int =
if (i < m.rows - 3 /\ i >= 0 /\ j < m.columns - 3 /\ j >= 0) then
Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3))))
else
None
function line (m: matrix int) (i: int) (j: int) : option int =
if (0 <= j < m.columns /\ i >= 0 /\ i < m.rows - 3) then
Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j))
else
None
function column (m: matrix int) (i: int) (j: int) : option int =
if (0 <= i < m.rows /\ j >= 0 /\ j < m.columns - 3) then
Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3)))
else
None
(** Computational functions for the product in each direction *)
let right_diag_c m i j : option int =
ensures {result = right_diag m i j}
if (i < m.rows - 3 && i >= 0 && j < m.columns - 3 && j >= 0) then
Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3))))
else
None
let left_diag_c m i j : option int =
ensures {result = left_diag m i j}
if (i < m.rows && j >= 0 && i >= 3 && j < m.columns - 3) then
Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3))))
else
None
let line_c m i j : option int =
ensures {result = line m i j}
if (0 <= j && j < m.columns && i >= 0 && i < m.rows - 3) then
Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j))
else
None
let column_c m i j : option int =
ensures {result = column m i j}
if (0 <= i && i < m.rows && j >= 0 && j < m.columns - 3) then
Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3)))
else
None
(* function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int = *)
(* match d with *)
(* | Left_bottom -> left_diag m i j *)
(* | Right_bottom -> right_diag m i j *)
(* | Bottom -> column m i j *)
(* | Right -> line m i j *)
(* end *)
(* TODO Failed attempt at pattern matching above. Combination of mathematical product result functions *)
function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int =
if (d = Left_bottom) then left_diag m i j
else if (d = Right_bottom) then right_diag m i j
else if (d = Bottom) then column m i j
else if (d = Right) then line m i j
else None
(** A product is_valid if each elements of the product is in the matrix *)
(* predicate is_valid (m: matrix int) (i: int) (j: int) (d: direction) = *)
(* match d with *)
(* | Left_bottom -> i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3 *)
(* | Right_bottom -> i >= 0 /\ j >= 0 /\ i < m.rows - 3 /\ j < m.columns - 3 *)
(* | Bottom -> 0 <= i /\ i < m.rows /\ j >= 0 /\ j < m.columns - 3 *)
(* | Right -> 0 <= j /\ j < m.columns /\ i >= 0 /\ i < m.rows - 3 *)
(* end *)
(** Return the maximum product of 4 for matrix m *)
let find_max (m: matrix int) =
requires {m.rows > 4 /\ m.columns > 4}
ensures {forall i j d. match (compute4 m i j d) with
| None -> true
| Some v -> v <= result
end}
ensures {exists i j d. Some result = compute4 m i j d}
(** Current max and element of the matrix for which it is attained *)
let cur_max = ref (
match (line_c m 0 0) with
| None -> 0 (* TODO should not happen *)
| Some v -> v
end) in
let cur_i = ref 0 in
let cur_j = ref 0 in
let cur_d = ref Right in
for i = 0 to (m.rows - 1) do
(* Cur_max is greater than each product already seen *)
invariant { forall i' j' d. (0 <= i' < i /\ 0 <= j' < m.columns) ->
match (compute4 m i' j' d) with
| None -> true
| Some v -> v <= !cur_max
end}
(* cur_max is actually the product at (cur_i, cur_j, cur_d) *)
invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d}
for j = 0 to (m.columns - 1) do
(* cur_max is actually the product at (cur_i, cur_j, cur_d) *)
invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d}
(* Cur_max is greater than each product already seen *)
invariant { forall i' j' d. ((i' = i /\ 0 <= j' /\ j' < j) \/ (0 <= i' < i /\ 0 <= j' < m.columns)) ->
match (compute4 m i' j' d) with
| None -> true
| Some v -> v <= !cur_max
end}
(* Computation of the product for each direction *)
match (left_diag_c m i j) with
| None -> ()
| Some v ->
if (v > !cur_max) then
begin
cur_max := v;
cur_i := i;
cur_j := j;
cur_d := Left_bottom;
end
end;
match (right_diag_c m i j) with
| None -> ()
| Some v ->
if (v > !cur_max) then
begin
cur_max := v;
cur_i := i;
cur_j := j;
cur_d := Right_bottom;
end
end;
match (line_c m i j) with
| None -> ()
| Some v ->
if (v > !cur_max) then
begin
cur_max := v;
cur_i := i;
cur_j := j;
cur_d := Right;
end
end;
match (column_c m i j) with
| None -> ()
| Some v ->
if (v > !cur_max) then
begin
cur_max := v;
cur_i := i;
cur_j := j;
cur_d := Bottom;
end
end;
done;
done;
(** Assert implying directly the postcondition *)
assert { Some !cur_max = compute4 m !cur_i !cur_j !cur_d};
!cur_max;;
*)
end
This diff is collapsed.
SHELL=/bin/bash
REPLAY=why3 replay -L .
MLW=base choice ho_set ho_rel fn order transfinite game game_fmla
REPLAY=why3 replay -L . -f
MLW=base choice ho_set ho_rel fn order transfinite game game_fmla transition
replay:
@exe() { echo "$$0 $$@"; "$$@"; };\
......
(* TODO: complete.... if feasible. *)
module Base
meta compute_max_steps 0x1_000_000
function f (x:('a,'b)) : 'a = let (x,_) = x in x
meta rewrite_def function f
function s (x:('a,'b)) : 'b = let (_,x) = x in x
meta rewrite_def function s
predicate (-->) (x y:'a) = "rewrite" (x = y)
meta rewrite_def predicate (-->)
end
(* Decomposition of quantification statements by destructuring
the argument structure. This is intended to be used by compute alone,
so the definitions/lemmas are kept away from the provers sight. *)
module Quant "W:non_conservative_extension:N"
use import HighOrd
use import int.Int
type qstructure 'a
predicate quant_structure bool (qstructure 'a) (p:'a -> bool)
val ghost quant_structure_def (_:'a -> bool) : unit
ensures { forall b s,p:'a -> bool.
quant_structure b s p <-> if b then forall y. p y else exists y. p y }
(* Unstructured quantification. *)
constant q_def : qstructure 'a
axiom forall_default : forall p:'a -> bool.
quant_structure true q_def p <-> forall y. p y
axiom exists_default : forall p:'a -> bool.
quant_structure false q_def p <-> exists y. p y
meta rewrite prop forall_default
meta rewrite prop exists_default
meta remove_prop prop forall_default
meta remove_prop prop exists_default
(* Unit quantification. *)
constant q_unit : qstructure unit
axiom quant_structure_unit : forall b p.
quant_structure b q_unit p <-> p ()
meta rewrite prop quant_structure_unit
meta remove_prop prop quant_structure_unit
(* Splitting pairs *)
function q_pair (qstructure 'a) (qstructure 'b) : qstructure ('a,'b)
axiom quant_structure_pair : forall b s1 s2,p:('a,'b) -> bool.
quant_structure b (q_pair s1 s2) p <->
quant_structure b s1 (\x. quant_structure b s2 (\y. p (x,y)))
meta rewrite prop quant_structure_pair
meta remove_prop prop quant_structure_pair
(* Boolean casing *)
function q_cond (qstructure 'a) (qstructure 'a) : qstructure ('a,bool)
axiom forall_cond : forall s1 s2,p:('a,bool) -> bool.
quant_structure true (q_cond s1 s2) p <->
quant_structure true s1 (\x. p (x,true)) /\
quant_structure true s2 (\x. p (x,false))
axiom exists_cond : forall s1 s2,p:('a,bool) -> bool.
quant_structure false (q_cond s1 s2) p <->
quant_structure false s1 (\x. p (x,true)) \/
quant_structure false s2 (\x. p (x,false))
meta rewrite prop forall_cond
meta rewrite prop exists_cond
meta remove_prop prop forall_cond
meta remove_prop prop exists_cond
(* Integer casing *)
function q_range int int (qstructure int) : qstructure int
predicate q_range_structure bool (qstructure int) int int int (int -> bool)
axiom quant_structure_range : forall b s n m,p:int -> bool.
quant_structure b (q_range n m s) p <-> q_range_structure b s n n m p
axiom forall_range_structure : forall s n l m,p:int -> bool.
q_range_structure true s n l m p =
if l = m then quant_structure true s (\x. not(n <= x < m) -> p x)
else p l /\ q_range_structure true s n (l+1) m p
axiom exists_range_structure : forall s n l m,p:int -> bool.
q_range_structure false s n l m p =
if l = m then quant_structure false s (\x. not(n <= x < m) /\ p x)
else p l \/ q_range_structure false s n (l+1) m p
meta rewrite prop quant_structure_range
meta rewrite prop forall_range_structure
meta rewrite prop exists_range_structure
meta remove_prop prop quant_structure_range
meta remove_prop prop forall_range_structure
meta remove_prop prop exists_range_structure
end
module QuantImpl
use import HighOrd
use import int.Int
type qstructure 'a = int
constant q_def : int = 0
function q_pair 'a 'b : int = 0
predicate quant_structure (b:bool) 'b (p:'a -> bool) =
if b then forall x. p x else exists x. p x
let ghost quant_structure_def (_:'b) = ()
function q_range 'a 'b 'c : int = 0
predicate q_range_structure (b:bool) 'a (n i m:int) (p:int -> bool) =
if b then forall x. not(n <= x < i) -> p x
else exists x. not (n <= x < i) /\ p x
clone Quant with type qstructure = qstructure,
predicate quant_structure = quant_structure,
val quant_structure_def = quant_structure_def,
function q_def = q_def,
goal forall_default,
goal exists_default,
function q_unit = q_def,
goal quant_structure_unit,
function q_pair = q_pair,
goal quant_structure_pair,
function q_cond = q_pair,
goal forall_cond,
goal exists_cond,
function q_range = q_range,
predicate q_range_structure = q_range_structure,
goal quant_structure_range,
goal forall_range_structure,
goal exists_range_structure
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compute_elts.mlw">
<theory name="Base" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Quant" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="QuantImpl" sum="43b1dc380e604d26ccd15795dd6d972d">
<goal name="WP_parameter quant_structure_def" expl="VC for quant_structure_def">
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="Quant.forall_default">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="Quant.exists_default">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Quant.quant_structure_unit">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="Quant.quant_structure_pair">
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="Quant.forall_cond">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Quant.exists_cond">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Quant.quant_structure_range">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="Quant.forall_range_structure">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Quant.exists_range_structure">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Quant.WP_parameter Quant quant_structure_def" expl="VC for Quant quant_structure_def">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
</theory>
</file>
</why3session>
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -201,7 +201,7 @@
<goal name="chain_subchain_completion">
<transf name="split_goal_wp">
<goal name="chain_subchain_completion.1" expl="1.">
<proof prover="2"><result status="valid" time="0.05" steps="357"/></proof>
<proof prover="2"><result status="valid" time="0.16" steps="357"/></proof>
</goal>
<goal name="chain_subchain_completion.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -219,7 +219,7 @@