# HG changeset patch
# User haftmann
# Date 1373730838 -7200
# Node ID 1501ebe39711e7d4976d92dedff0a5c546931fc2
# Parent  238cec044ebf1c8382523b93144f5a7429d80cb8
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead

diff -r 238cec044ebf -r 1501ebe39711 NEWS
--- a/NEWS	Sat Jul 13 17:53:57 2013 +0200
+++ b/NEWS	Sat Jul 13 17:53:58 2013 +0200
@@ -84,6 +84,9 @@
 
 *** HOL ***
 
+* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.
+Use explicit 'code equation' and 'code abstract' to distinguish both when desired.
+
 * Code generator:
   * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
   * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
diff -r 238cec044ebf -r 1501ebe39711 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Sat Jul 13 17:53:57 2013 +0200
+++ b/src/Doc/Codegen/Refinement.thy	Sat Jul 13 17:53:58 2013 +0200
@@ -236,7 +236,7 @@
   \noindent This we have to prove indirectly as follows:
 *}
 
-lemma %quote [code abstract]:
+lemma %quote [code]:
   "list_of_dlist Dlist.empty = []"
   by (fact list_of_dlist_empty)
 
@@ -247,11 +247,11 @@
   similar:
 *}
 
-lemma %quote [code abstract]:
+lemma %quote [code]:
   "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
   by (fact list_of_dlist_insert)
 
-lemma %quote [code abstract]:
+lemma %quote [code]:
   "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
   by (fact list_of_dlist_remove)
 
@@ -261,7 +261,7 @@
 
 text %quotetypewriter {*
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
-*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
+*}
 
 text {*
   Typical data structures implemented by representations involving
diff -r 238cec044ebf -r 1501ebe39711 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Sat Jul 13 17:53:57 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Sat Jul 13 17:53:58 2013 +0200
@@ -2242,7 +2242,7 @@
     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
 
-    @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
+    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' )?
     ;
 
     @@{command (HOL) code_abort} ( const + )
@@ -2397,12 +2397,18 @@
   ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
   datatype declaration.
 
-  \item @{attribute (HOL) code} explicitly selects (or with option
-  ``@{text "del"}'' deselects) a code equation for code generation.
-  Usually packages introducing code equations provide a reasonable
-  default setup for selection.  Variants @{text "code abstype"} and
+  \item @{attribute (HOL) code} declare code equations for code
+  generation.  Variant @{text "code equation"} declares a conventional
+  equation as code equation.  Variants @{text "code abstype"} and
   @{text "code abstract"} declare abstract datatype certificates or
   code equations on abstract datatype representations respectively.
+  Vanilla @{text "code"} falls back to @{text "code equation"}
+  or @{text "code abstype"} depending on the syntactic shape
+  of the underlying equation.  Variant @{text "code del"}
+  deselects a code equation for code generation.
+
+  Usually packages introducing code equations provide a reasonable
+  default setup for selection.  
 
   \item @{command (HOL) "code_abort"} declares constants which are not
   required to have a definition by means of code equations; if needed
diff -r 238cec044ebf -r 1501ebe39711 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jul 13 17:53:57 2013 +0200
+++ b/src/Pure/Isar/code.ML	Sat Jul 13 17:53:58 2013 +0200
@@ -22,7 +22,6 @@
 
   (*code equations and certificates*)
   val mk_eqn: theory -> thm * bool -> thm * bool
-  val mk_eqn_warning: theory -> thm -> (thm * bool) option
   val mk_eqn_liberal: theory -> thm -> (thm * bool) option
   val assert_eqn: theory -> thm * bool -> thm * bool
   val const_typ_eqn: theory -> thm -> string * typ
@@ -535,7 +534,9 @@
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
           else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
       | NONE => ();
-    val (vs', (_, (rep', _))) = get_abstype_spec thy tyco;
+    val (vs', (_, (rep', _))) = case try (get_abstype_spec thy) tyco
+     of SOME data => data
+      | NONE => bad_thm ("Not an abstract type: " ^ tyco);
     val _ = if rep_const = rep' then ()
       else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     val _ = check_eqn thy { allow_nonlinear = false,
@@ -551,12 +552,19 @@
 fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o
   apfst (meta_rewrite thy);
 
-fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm))
-  o warning_thm (gen_assert_eqn thy false) thy o rpair false o meta_rewrite thy;
-
 fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
 
+fun mk_eqn_maybe_abs thy raw_thm =
+  let
+    val thm = meta_rewrite thy raw_thm;
+    val some_abs_thm = try_thm (assert_abs_eqn thy NONE) thm;
+  in case some_abs_thm
+   of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
+    | NONE => (Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
+        o warning_thm (gen_assert_eqn thy false) thy) (thm, false)
+  end;
+
 fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn thy NONE) thy o meta_rewrite thy;
 
 val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -1060,14 +1068,15 @@
       | add_eqn' false _ = Eqns [(thm, proper)];
   in change_fun_spec false c (add_eqn' default) thy end;
 
+fun gen_add_abs_eqn raw_thm thy =
+  let
+    val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm;
+    val c = const_abs_eqn thy abs_thm;
+  in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end;
+
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, true)) thy;
 
-fun add_warning_eqn thm thy =
-  case mk_eqn_warning thy thm
-   of SOME eqn => gen_add_eqn false eqn thy
-    | NONE => thy;
-
 fun add_nbe_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, false)) thy;
 
@@ -1087,11 +1096,13 @@
   (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
 val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
 
-fun add_abs_eqn raw_thm thy =
-  let
-    val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;
-    val c = const_abs_eqn thy abs_thm;
-  in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end;
+fun add_abs_eqn raw_thm thy = gen_add_abs_eqn (mk_abs_eqn thy raw_thm) thy;
+
+fun add_eqn_maybe_abs thm thy =
+  case mk_eqn_maybe_abs thy thm
+   of SOME (eqn, NONE) => gen_add_eqn false eqn thy
+    | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn (thm, tyco) thy
+    | NONE => thy;
 
 fun del_eqn thm thy = case mk_eqn_liberal thy thm
  of SOME (thm, _) => let
@@ -1226,10 +1237,11 @@
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     val code_attribute_parser =
       Args.del |-- Scan.succeed (mk_attribute del_eqn)
+      || Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_eqn)
       || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
       || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
       || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
-      || Scan.succeed (mk_attribute add_warning_eqn);
+      || Scan.succeed (mk_attribute add_eqn_maybe_abs);
   in
     Datatype_Interpretation.init
     #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)