Commit 18c56fdb authored by MARCHE Claude's avatar MARCHE Claude

Updated Isabelle realization of BV: disabled until someone's able to complete it

parent 1e02629b
......@@ -638,6 +638,7 @@ gallery::
GALLERYSUBS=avl
gallery-subs::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for d in $(GALLERYSUBS) ; do \
echo "exporting examples/$$d"; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
......@@ -654,7 +655,7 @@ gallery-subs::
x=$*/why3session.xml; \
d=`dirname $$x`; \
f=`basename $$d`; \
why3 session html $$x; \
why3 session html $$d; \
echo "exporting $$f"; \
mkdir -p $(GALLERYDIR)/$$f; \
if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
......@@ -1201,8 +1202,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_OPTION_FILES); do \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
# for f in $(ISABELLELIBS_BV_FILES); do \
# echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
) > $@
ifeq (@enable_local@,yes)
......@@ -1211,7 +1212,8 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
# $(ISABELLELIBS_BV)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
......
......@@ -6,7 +6,7 @@ imports
Why3_Int
Why3_Bool
Why3_Number
Why3_BV
(* Why3_BV *)
Why3_Real
begin
......
......@@ -336,7 +336,7 @@ why3_vc to_uint_urem
by (simp add: uint_mod emod_def)
why3_vc Nth_rotate_left
using assms rotl_nth [of "unat n" v "unat i"]
using assms rotl_nth [of "nat n" v "nat i"]
apply (simp add: ult_def unat_mod)
apply (simp only: word_arith_nat_add unat_of_nat)
apply (simp add: mod_mod_cancel uint_nat)
......@@ -401,6 +401,8 @@ why3_open "bv/BV16.xml"
lsl_bv=lsl_bv
rotate_left=rotate_left
rotate_right=rotate_right
rotate_left_bv=rotate_left_bv
rotate_right_bv=rotate_right_bv
nth=bv_nth
nth_bv=nth_bv
to_uint=uint
......@@ -572,6 +574,8 @@ why3_open "bv/BV32.xml"
lsl_bv=lsl_bv
rotate_left=rotate_left
rotate_right=rotate_right
rotate_left_bv=rotate_left_bv
rotate_right_bv=rotate_right_bv
nth=bv_nth
nth_bv=nth_bv
to_uint=uint
......@@ -743,6 +747,8 @@ why3_open "bv/BV64.xml"
lsl_bv=lsl_bv
rotate_left=rotate_left
rotate_right=rotate_right
rotate_left_bv=rotate_left_bv
rotate_right_bv=rotate_right_bv
nth=bv_nth
nth_bv=nth_bv
to_uint=uint
......
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