From 18c56fdb31a64e7cfef1e814f26da0b56a730449 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 20 Nov 2015 11:03:13 +0100
Subject: [PATCH] Updated Isabelle realization of BV: disabled until someone's
 able to complete it

---
 Makefile.in              | 10 ++++++----
 lib/isabelle/Why3.thy    |  2 +-
 lib/isabelle/Why3_BV.thy |  8 +++++++-
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index 1d5221210..31ce34de0 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -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
diff --git a/lib/isabelle/Why3.thy b/lib/isabelle/Why3.thy
index 27f4c8ec6..340832b2c 100644
--- a/lib/isabelle/Why3.thy
+++ b/lib/isabelle/Why3.thy
@@ -6,7 +6,7 @@ imports
   Why3_Int
   Why3_Bool
   Why3_Number
-  Why3_BV
+(*  Why3_BV *)
   Why3_Real
 begin
 
diff --git a/lib/isabelle/Why3_BV.thy b/lib/isabelle/Why3_BV.thy
index 50e272b1e..55a5d38b2 100644
--- a/lib/isabelle/Why3_BV.thy
+++ b/lib/isabelle/Why3_BV.thy
@@ -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
-- 
GitLab