fundamental treatment of undefined vs. universally partial replaces code_abort

--- a/NEWS	Wed Jan 01 01:05:46 2014 +0100
+++ b/NEWS	Wed Jan 01 01:05:48 2014 +0100
@@ -33,6 +33,12 @@
 
 *** HOL ***
 
+* "declare [[code abort: …]]" replaces "code_abort …".
+INCOMPATIBILITY.
+
+* "declare [[code drop: …]]" drops all code equations associated
+with the given constants.
+
 * Abolished slightly odd global lattice interpretation for min/max.
 
 Fact consolidations:

--- a/src/Doc/Codegen/Foundations.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/Doc/Codegen/Foundations.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -308,10 +308,11 @@
   of as function definitions which always fail,
   since there is never a successful pattern match on the left hand
   side.  In order to categorise a constant into that category
-  explicitly, use @{command_def "code_abort"}:
+  explicitly, use the @{attribute code} attribute with
+  @{text abort}:
 *}
 
-code_abort %quote empty_queue
+declare %quote [[code abort: empty_queue]]
 
 text {*
   \noindent Then the code generator will just insert an error or
@@ -324,9 +325,9 @@
 
 text {*
   \noindent This feature however is rarely needed in practice.  Note
-  also that the HOL default setup already declares @{const undefined}
-  as @{command "code_abort"}, which is most likely to be used in such
-  situations.
+  also that the HOL default setup already declares @{const undefined},
+  which is most likely to be used in such situations, as
+  @{text "code abort"}.
 *}
 
 

--- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -2391,7 +2391,6 @@
   \begin{matharray}{rcl}
     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def (HOL) code} & : & @{text attribute} \\
-    @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
@@ -2435,10 +2434,8 @@
     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
 
-    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' )?
-    ;
-
-    @@{command (HOL) code_abort} ( const + )
+    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
+      | 'drop:' ( const + ) | 'abort:' ( const + ) )?
     ;
 
     @@{command (HOL) code_datatype} ( const + )
@@ -2600,13 +2597,15 @@
   of the underlying equation.  Variant @{text "code del"}
   deselects a code equation for code generation.
 
+  Variants @{text "code drop:"} and @{text "code abort:"} take
+  a list of constant as arguments and drop all code equations declared
+  for them.  In the case of {text abort}, these constants then are
+  are not required to have a definition by means of code equations;
+  if needed these are implemented by program abort (exception) instead.
+
   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
-  these are implemented by program abort instead.
-
   \item @{command (HOL) "code_datatype"} specifies a constructor set
   for a logical type.
 

--- a/src/HOL/Enum.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/Enum.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -116,7 +116,7 @@
     unfolding enum_the_def by (auto split: list.split)
 qed
 
-code_abort enum_the
+declare [[code abort: enum_the]]
 
 code_printing
   constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"

--- a/src/HOL/HOL.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -1832,7 +1832,7 @@
   #> Code.add_undefined @{const_name undefined}
 *}
 
-code_abort undefined
+declare [[code abort: undefined]]
 
 
 subsubsection {* Generic code generator target languages *}

--- a/src/HOL/Library/Product_Vector.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -87,7 +87,7 @@
 
 end
 
-code_abort "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"
+declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
 
 lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
 unfolding open_prod_def by auto
@@ -346,7 +346,7 @@
 
 end
 
-code_abort "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"
+declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
 
 lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
   unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
@@ -426,7 +426,7 @@
 
 end
 
-code_abort "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"
+declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
 
 instance prod :: (banach, banach) banach ..
 

--- a/src/HOL/List.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/List.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -6133,7 +6133,7 @@
 
 definition "abort_Bleast S P = (LEAST x. x \<in> S \<and> P x)"
 
-code_abort abort_Bleast
+declare [[code abort: abort_Bleast]]
 
 lemma Bleast_code [code]:
  "Bleast (set xs) P = (case filter P (sort xs) of

--- a/src/HOL/Real_Vector_Spaces.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -968,7 +968,7 @@
 
 end
 
-code_abort "open :: real set \<Rightarrow> bool"
+declare [[code abort: "open :: real set \<Rightarrow> bool"]]
 
 instance real :: linorder_topology
 proof

--- a/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:48 2014 +0100
@@ -64,7 +64,6 @@
   val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
   val add_include: string -> string * (string * string list) option -> theory -> theory
-  val allow_abort: string -> theory -> theory
 
   val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -231,23 +230,20 @@
 
 structure Targets = Theory_Data
 (
-  type T = (target Symtab.table * string list) * int;
-  val empty = ((Symtab.empty, []), 80);
+  type T = target Symtab.table * int;
+  val empty = (Symtab.empty, 80);
   val extend = I;
-  fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T =
-    ((Symtab.join (merge_target true) (target1, target2),
-      Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
+  fun merge ((target1, width1), (target2, width2)) : T =
+    (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
 );
 
-val abort_allowed = snd o fst o Targets.get;
-
-fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
+fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target
   then target
   else error ("Unknown code target language: " ^ quote target);
 
 fun put_target (target, seri) thy =
   let
-    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
+    val lookup_target = Symtab.lookup (fst (Targets.get thy));
     val _ = case seri
      of Extension (super, _) => if is_some (lookup_target super) then ()
           else error ("Unknown code target language: " ^ quote super)
@@ -263,7 +259,7 @@
       else ();
   in
     thy
-    |> (Targets.map o apfst o apfst o Symtab.update)
+    |> (Targets.map o apfst o Symtab.update)
         (target, make_target ((serial (), seri),
           ([], (Code_Symbol.empty_data, Code_Symbol.empty_data))))
   end;
@@ -277,7 +273,7 @@
     val _ = assert_target thy target;
   in
     thy
-    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target o apsnd) f
+    |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f
   end;
 
 fun map_reserved target =
@@ -296,7 +292,7 @@
 
 fun the_fundamental thy =
   let
-    val ((targets, _), _) = Targets.get thy;
+    val (targets, _) = Targets.get thy;
     fun fundamental target = case Symtab.lookup targets target
      of SOME data => (case the_description data
          of Fundamental data => data
@@ -308,7 +304,7 @@
 
 fun collapse_hierarchy thy =
   let
-    val ((targets, _), _) = Targets.get thy;
+    val (targets, _) = Targets.get thy;
     fun collapse target =
       let
         val data = case Symtab.lookup targets target
@@ -326,9 +322,9 @@
 
 fun activate_target thy target =
   let
-    val ((_, abortable), default_width) = Targets.get thy;
+    val (_, default_width) = Targets.get thy;
     val (modify, data) = collapse_hierarchy thy target;
-  in (default_width, abortable, data, modify) end;
+  in (default_width, data, modify) end;
 
 fun activate_const_syntax thy literals cs_data naming =
   (Symtab.empty, naming)
@@ -363,14 +359,13 @@
       (const_syntax, tyco_syntax, class_syntax))
   end;
 
-fun project_program thy abortable names_hidden names1 program2 =
+fun project_program thy names_hidden names1 program2 =
   let
     val ctxt = Proof_Context.init_global thy;
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
     val names4 = Graph.all_succs program3 names2;
-    val unimplemented = filter_out (member (op =) abortable)
-      (Code_Thingol.unimplemented program3);
+    val unimplemented = Code_Thingol.unimplemented program3;
     val _ =
       if null unimplemented then ()
       else error ("No code equations for " ^
@@ -378,12 +373,12 @@
     val program4 = Graph.restrict (member (op =) names4) program3;
   in (names4, program4) end;
 
-fun prepare_serializer thy abortable (serializer : serializer) literals reserved identifiers
+fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
     printings module_name args naming proto_program names =
   let
     val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
       activate_symbol_syntax thy literals naming printings;
-    val (names_all, program) = project_program thy abortable names_hidden names proto_program;
+    val (names_all, program) = project_program thy names_hidden names proto_program;
     fun select_include (name, (content, cs)) =
       if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
        of SOME name => member (op =) names_all name
@@ -405,11 +400,11 @@
 
 fun mount_serializer thy target some_width module_name args naming program names =
   let
-    val (default_width, abortable, data, modify) = activate_target thy target;
+    val (default_width, data, modify) = activate_target thy target;
     val serializer = case the_description data
      of Fundamental seri => #serializer seri;
     val (prepared_serializer, prepared_program) =
-      prepare_serializer thy abortable serializer (the_literals thy target)
+      prepare_serializer thy serializer (the_literals thy target)
         (the_reserved data) (the_identifiers data) (the_printings data)
         module_name args naming (modify naming program) names
     val width = the_default default_width some_width;
@@ -502,7 +497,7 @@
 
 fun implemented_functions thy naming program =
   let
-    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.unimplemented program);
+    val cs = Code_Thingol.unimplemented program;
     val names = map_filter (Code_Thingol.lookup_const naming) cs;
   in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
 
@@ -699,14 +694,6 @@
     target name some_content thy;
 
 
-(* abortable constants *)
-
-fun gen_allow_abort prep_const raw_c thy =
-  let
-    val c = prep_const thy raw_c;
-  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
-
-
 (* concrete syntax *)
 
 local
@@ -732,14 +719,12 @@
 val add_class_syntax = gen_add_class_syntax cert_class;
 val add_instance_syntax = gen_add_instance_syntax cert_inst;
 val add_include = gen_add_include (K I);
-val allow_abort = gen_allow_abort (K I);
 
 val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
 val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
 val add_class_syntax_cmd = gen_add_class_syntax read_class;
 val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
 val add_include_cmd = gen_add_include Code.read_const;
-val allow_abort_cmd = gen_allow_abort Code.read_const;
 
 fun parse_args f args =
   case Scan.read Token.stopper f args
@@ -842,11 +827,6 @@
           (Toplevel.theory o add_include_cmd target) (name, content_consts)));
 
 val _ =
-  Outer_Syntax.command @{command_spec "code_abort"}
-    "permit constant to be implemented as program abort"
-    (Scan.repeat1 Parse.term >> (Toplevel.theory o fold allow_abort_cmd));
-
-val _ =
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
     (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 

--- a/src/Tools/Code_Generator.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/Tools/Code_Generator.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -10,7 +10,7 @@
   "value" "print_codeproc" "code_thms" "code_deps" :: diag and
   "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
     "code_const" "code_reserved" "code_include" "code_modulename"
-    "code_abort" "code_monad" "code_reflect" :: thy_decl and
+    "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"
   "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
 begin