Dear Isabelle developers,
I'm currently running some trials for my custom code preprocessor.
Internally, I use the "deriving" mechanism to obtain a linear ordering
for some of my types. While doing that, I noticed that just importing
"$AFP/Datatype_Order_Generator/Derive"
pulls in code setup for natural numbers (in a way with which I can't
deal yet). In my case, the fix was simple; I just had to change the
import to
"$AFP/Datatype_Order_Generator/Order_Generator"
The code setup came in via "$AFP/Collections/Lib/HashCode". I've created
a patch to afp-devel which removes the code setup there.
This is a potentially far-reaching change because we currently don't
test for concrete code setup, and this might introduce silent
performance regressions in generated code. I've spoken to Peter and he
seems okay with it as long as the code setup is retained in all other
places in the AFP (see attached patch).
Before pushing this patch to the AFP I wanted to make sure that nobody
else is affected by this change.
Cheers
Lars
# HG changeset patch
# User Lars Hupel <lars.hu...@mytum.de>
# Date 1490094521 -3600
# Tue Mar 21 12:08:41 2017 +0100
# Node ID e0065e482c765059bb4cf2ba1378f5dedb548d99
# Parent e1df3d2838ded6d6d9da76c7dce4618fe7ddfb7a
remove useless import
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy
--- a/thys/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy Tue Mar 21 12:08:41 2017 +0100
@@ -6,6 +6,7 @@
"../Intf/Intf_Hash"
"../Intf/Intf_Map"
"../../Lib/HashCode"
+ "../../Lib/Code_Target_ICF"
"../../Lib/Diff_Array"
Impl_List_Map
begin
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/GenCF/Intf/Intf_Hash.thy
--- a/thys/Collections/GenCF/Intf/Intf_Hash.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/GenCF/Intf/Intf_Hash.thy Tue Mar 21 12:08:41 2017 +0100
@@ -3,6 +3,7 @@
imports
Main
"../../Lib/HashCode"
+ "../../Lib/Code_Target_ICF"
"../../../Automatic_Refinement/Automatic_Refinement"
begin
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/ICF/impl/ArrayHashMap_Impl.thy
--- a/thys/Collections/ICF/impl/ArrayHashMap_Impl.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/ICF/impl/ArrayHashMap_Impl.thy Tue Mar 21 12:08:41 2017 +0100
@@ -5,6 +5,7 @@
section {* \isaheader{Array-based hash map implementation} *}
theory ArrayHashMap_Impl imports
"../../Lib/HashCode"
+ "../../Lib/Code_Target_ICF"
"../../Lib/Diff_Array"
"../gen_algo/ListGA"
"ListMapImpl"
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/ICF/impl/HashMap_Impl.thy
--- a/thys/Collections/ICF/impl/HashMap_Impl.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/ICF/impl/HashMap_Impl.thy Tue Mar 21 12:08:41 2017 +0100
@@ -8,6 +8,7 @@
RBTMapImpl
ListMapImpl
"../../Lib/HashCode"
+ "../../Lib/Code_Target_ICF"
begin
text {*
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/Lib/HashCode.thy
--- a/thys/Collections/Lib/HashCode.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/Lib/HashCode.thy Tue Mar 21 12:08:41 2017 +0100
@@ -6,7 +6,6 @@
theory HashCode
imports
"../../Native_Word/Uint32"
- "Code_Target_ICF"
begin
text_raw {*\label{thy:HashCode}*}
@@ -148,4 +147,4 @@
hide_type (open) word
-end
+end
\ No newline at end of file
diff -r e1df3d2838de -r e0065e482c76 thys/Collections/ROOT
--- a/thys/Collections/ROOT Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Collections/ROOT Tue Mar 21 12:08:41 2017 +0100
@@ -15,6 +15,7 @@
(* Libraries and Tools *)
"Lib/Sorted_List_Operations"
"Lib/HashCode"
+ "Lib/Code_Target_ICF"
"Lib/RBT_add"
"Lib/Dlist_add"
"Lib/Assoc_List"
diff -r e1df3d2838de -r e0065e482c76 thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy Tue Mar 21 12:08:41 2017 +0100
@@ -1,6 +1,9 @@
section "Hash-Tables"
theory Hash_Table
-imports "../../Collections/Lib/HashCode" "../Sep_Main"
+imports
+ "../../Collections/Lib/HashCode"
+ "../../Collections/Lib/Code_Target_ICF"
+ "../Sep_Main"
begin
subsection {* Datatype *}
diff -r e1df3d2838de -r e0065e482c76 thys/Separation_Logic_Imperative_HOL/ROOT
--- a/thys/Separation_Logic_Imperative_HOL/ROOT Mon Mar 20 13:53:46 2017 +0100
+++ b/thys/Separation_Logic_Imperative_HOL/ROOT Tue Mar 21 12:08:41 2017 +0100
@@ -6,6 +6,7 @@
"Tools/Imperative_HOL_Add"
"Tools/Syntax_Match"
"../Collections/Lib/HashCode"
+ "../Collections/Lib/Code_Target_ICF"
"../Automatic_Refinement/Lib/Misc"
"Tools/Sep_Misc"
theories
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
