# HG changeset patch
# User haftmann
# Date 1423208868 -3600
# Node ID 792272e6ee6b0204f72329300f38fe4e8b9a621a
# Parent  a130ae7a93988345ac9f37f2b53acf2c92f0fc27
non-intrusive default code setup for mappings

diff -r a130ae7a9398 -r 792272e6ee6b src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu Feb 05 19:44:14 2015 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Feb 06 08:47:48 2015 +0100
@@ -98,7 +98,7 @@
   morphisms rep Mapping
   ..
 
-setup_lifting (no_code) type_definition_mapping
+setup_lifting type_definition_mapping
 
 lift_definition empty :: "('a, 'b) mapping"
   is Map.empty parametric empty_parametric .
@@ -106,6 +106,9 @@
 lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option"
   is "\<lambda>m k. m k" parametric lookup_parametric .
 
+declare [[code drop: Mapping.lookup]]
+setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close>
+
 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
 
@@ -124,6 +127,8 @@
 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping"
   is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric .
 
+declare [[code drop: map]]
+
 
 subsection {* Functorial structure *}
 
@@ -405,9 +410,8 @@
 
 subsection {* Code generator setup *}
 
-code_datatype empty update
-
 hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
   replace default map_entry map_default tabulate bulkload map of_alist
 
 end
+