# HG changeset patch
# User haftmann
# Date 1388534746 -3600
# Node ID 4121d64fde90ef8513712f5c7a548201b8a17589
# Parent  6edabf38d929bc73e96fb3efdeb12fb3c347a274
explicit distinction between empty code equations and no code equations, including convenient declaration attributes

diff -r 6edabf38d929 -r 4121d64fde90 src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -35,6 +35,7 @@
     val thms = Code_Preproc.cert eqngr const
       |> Code.equations_of_cert thy
       |> snd
+      |> these
       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
       |> map (holize o no_vars ctxt o Axclass.overload thy);
   in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
diff -r 6edabf38d929 -r 4121d64fde90 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Pure/Isar/code.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -31,7 +31,7 @@
   val conclude_cert: cert -> cert
   val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
   val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
-    * (((term * string option) list * (term * string option)) * (thm option * bool)) list
+    * (((term * string option) list * (term * string option)) * (thm option * bool)) list option
   val pretty_cert: theory -> cert -> Pretty.T list
 
   (*executable code*)
@@ -55,6 +55,7 @@
   val add_nbe_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
+  val del_exception: string -> theory -> theory
   val add_case: thm -> theory -> theory
   val add_undefined: string -> theory -> theory
   val get_type: theory -> string
@@ -175,6 +176,7 @@
       (* (cache for default equations, lazy computation of default equations)
          -- helps to restore natural order of default equations *)
   | Eqns of (thm * bool) list
+  | None
   | Proj of term * string
   | Abstr of thm * string;
 
@@ -719,12 +721,13 @@
 
 val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
 
-abstype cert = Equations of thm * bool list
+abstype cert = Nothing of thm
+  | Equations of thm * bool list
   | Projection of term * string
   | Abstract of thm * string
 with
 
-fun empty_cert thy c = 
+fun dummy_thm thy c =
   let
     val raw_ty = devarify (const_typ thy c);
     val (vs, _) = typscheme thy (c, raw_ty);
@@ -737,9 +740,11 @@
     val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
     val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
     val chead = build_head thy (c, ty);
-  in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
+  in Thm.weaken chead Drule.dummy_thm end;
 
-fun cert_of_eqns thy c [] = empty_cert thy c
+fun nothing_cert thy c = Nothing (dummy_thm thy c);
+
+fun cert_of_eqns thy c [] = Equations (dummy_thm thy c, [])
   | cert_of_eqns thy c raw_eqns = 
       let
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
@@ -780,38 +785,51 @@
         ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
   in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
 
-fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
-      let
-        val ((vs, _), head) = get_head thy cert_thm;
-        val (subst, cert_thm') = cert_thm
-          |> Thm.implies_intr head
-          |> constrain_thm thy vs sorts;
-        val head' = Thm.term_of head
-          |> subst
-          |> Thm.cterm_of thy;
-        val cert_thm'' = cert_thm'
-          |> Thm.elim_implies (Thm.assume head');
-      in Equations (cert_thm'', propers) end
+fun constrain_cert_thm thy sorts cert_thm =
+  let
+    val ((vs, _), head) = get_head thy cert_thm;
+    val (subst, cert_thm') = cert_thm
+      |> Thm.implies_intr head
+      |> constrain_thm thy vs sorts;
+    val head' = Thm.term_of head
+      |> subst
+      |> Thm.cterm_of thy;
+    val cert_thm'' = cert_thm'
+      |> Thm.elim_implies (Thm.assume head');
+  in cert_thm'' end;
+
+fun constrain_cert thy sorts (Nothing cert_thm) =
+      Nothing (constrain_cert_thm thy sorts cert_thm)
+  | constrain_cert thy sorts (Equations (cert_thm, propers)) =
+      Equations (constrain_cert_thm thy sorts cert_thm, propers)
   | constrain_cert thy _ (cert as Projection _) =
       cert
   | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
       Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
 
-fun conclude_cert (Equations (cert_thm, propers)) =
-      (Equations (Thm.close_derivation cert_thm, propers))
+fun conclude_cert (Nothing cert_thm) =
+      Nothing (Thm.close_derivation cert_thm)
+  | conclude_cert (Equations (cert_thm, propers)) =
+      Equations (Thm.close_derivation cert_thm, propers)
   | conclude_cert (cert as Projection _) =
       cert
   | conclude_cert (Abstract (abs_thm, tyco)) =
-      (Abstract (Thm.close_derivation abs_thm, tyco));
+      Abstract (Thm.close_derivation abs_thm, tyco);
 
-fun typscheme_of_cert thy (Equations (cert_thm, _)) =
+fun typscheme_of_cert thy (Nothing cert_thm) =
+      fst (get_head thy cert_thm)
+  | typscheme_of_cert thy (Equations (cert_thm, _)) =
       fst (get_head thy cert_thm)
   | typscheme_of_cert thy (Projection (proj, _)) =
       typscheme_projection thy proj
   | typscheme_of_cert thy (Abstract (abs_thm, _)) =
       typscheme_abs thy abs_thm;
 
-fun typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
+fun typargs_deps_of_cert thy (Nothing cert_thm) =
+      let
+        val vs = (fst o fst) (get_head thy cert_thm);
+      in (vs, []) end
+  | typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
       let
         val vs = (fst o fst) (get_head thy cert_thm);
         val equations = if null propers then [] else
@@ -826,7 +844,9 @@
         val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
       in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end;
 
-fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
+fun equations_of_cert thy (cert as Nothing _) =
+      (typscheme_of_cert thy cert, NONE)
+  | equations_of_cert thy (cert as Equations (cert_thm, propers)) =
       let
         val tyscm = typscheme_of_cert thy cert;
         val thms = if null propers then [] else
@@ -835,27 +855,29 @@
           |> Thm.varifyT_global
           |> Conjunction.elim_balanced (length propers);
         fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
-      in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+      in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end
   | equations_of_cert thy (Projection (t, tyco)) =
       let
         val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
         val tyscm = typscheme_projection thy t;
         val t' = Logic.varify_types_global t;
         fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
-      in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end
+      in (tyscm, SOME [((abstractions o dest_eqn) t', (NONE, true))]) end
   | equations_of_cert thy (Abstract (abs_thm, tyco)) =
       let
         val tyscm = typscheme_abs thy abs_thm;
         val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
         fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
       in
-        (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
+        (tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
           (SOME (Thm.varifyT_global abs_thm), true))])
       end;
 
-fun pretty_cert thy (cert as Equations _) =
+fun pretty_cert thy (cert as Nothing _) =
+      [Pretty.str "(not implemented)"]
+  | pretty_cert thy (cert as Equations _) =
       (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
-         o snd o equations_of_cert thy) cert
+         o these o snd o equations_of_cert thy) cert
   | pretty_cert thy (Projection (t, _)) =
       [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
   | pretty_cert thy (Abstract (abs_thm, _)) =
@@ -869,7 +891,7 @@
 fun retrieve_raw thy c =
   Symtab.lookup ((the_functions o the_exec) thy) c
   |> Option.map (snd o fst)
-  |> the_default initial_fun_spec
+  |> the_default None
 
 fun eqn_conv conv ct =
   let
@@ -893,12 +915,12 @@
 
 fun get_cert thy { functrans, ss } c =
   case retrieve_raw thy c
-   of Default (_, eqns_lazy) => Lazy.force eqns_lazy
+   of Default (eqns, eqns_lazy) => Lazy.force eqns_lazy
         |> cert_of_eqns_preprocess thy functrans ss c
     | Eqns eqns => eqns
         |> cert_of_eqns_preprocess thy functrans ss c
-    | Proj (_, tyco) =>
-        cert_of_proj thy c tyco
+    | None => nothing_cert thy c
+    | Proj (_, tyco) => cert_of_proj thy c tyco
     | Abstr (abs_thm, tyco) => abs_thm
         |> Thm.transfer thy
         |> rewrite_eqn thy Conv.arg_conv ss
@@ -966,6 +988,7 @@
     fun pretty_function (const, Default (_, eqns_lazy)) =
           pretty_equations const (map fst (Lazy.force eqns_lazy))
       | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
+      | pretty_function (const, None) = pretty_equations const []
       | pretty_function (const, Proj (proj, _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
       | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
@@ -1054,6 +1077,7 @@
       (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
     fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
+      | add_eqn' true None = Default (natural_order [(thm, proper)])
       | add_eqn' true fun_spec = fun_spec
       | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
       | add_eqn' false _ = Eqns [(thm, proper)];
@@ -1100,12 +1124,16 @@
       let
         fun del_eqn' (Default _) = initial_fun_spec
           | del_eqn' (Eqns eqns) =
-              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
+              let
+                val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
+              in if null eqns' then None else Eqns eqns' end
           | del_eqn' spec = spec
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;
 
-fun del_eqns c = change_fun_spec c (K initial_fun_spec);
+fun del_eqns c = change_fun_spec c (K None);
+
+fun del_exception c = change_fun_spec c (K (Eqns []));
 
 
 (* cases *)
@@ -1229,12 +1257,16 @@
 val _ = Theory.setup
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+    fun mk_const_attribute f cs =
+      mk_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
     val code_attribute_parser =
-      Args.del |-- Scan.succeed (mk_attribute del_eqn)
-      || Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_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)
+      || Args.del |-- Scan.succeed (mk_attribute del_eqn)
+      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_eqns)
+      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception)
       || Scan.succeed (mk_attribute add_eqn_maybe_abs);
   in
     Datatype_Interpretation.init
diff -r 6edabf38d929 -r 4121d64fde90 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -369,12 +369,12 @@
     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 empty_funs = filter_out (member (op =) abortable)
-      (Code_Thingol.empty_funs program3);
+    val unimplemented = filter_out (member (op =) abortable)
+      (Code_Thingol.unimplemented program3);
     val _ =
-      if null empty_funs then ()
+      if null unimplemented then ()
       else error ("No code equations for " ^
-        commas (map (Proof_Context.extern_const ctxt) empty_funs));
+        commas (map (Proof_Context.extern_const ctxt) unimplemented));
     val program4 = Graph.restrict (member (op =) names4) program3;
   in (names4, program4) end;
 
@@ -500,9 +500,9 @@
 
 (* code generation *)
 
-fun transitivly_non_empty_funs thy naming program =
+fun implemented_functions thy naming program =
   let
-    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
+    val cs = subtract (op =) (abort_allowed thy) (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;
 
@@ -510,7 +510,7 @@
   let
     val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
     val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
-    val names3 = transitivly_non_empty_funs thy naming program;
+    val names3 = implemented_functions thy naming program;
     val cs3 = map_filter (fn (c, name) =>
       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   in union (op =) cs3 cs1 end;
diff -r 6edabf38d929 -r 4121d64fde90 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -68,7 +68,7 @@
   val ensure_declared_const: theory -> string -> naming -> string * naming
 
   datatype stmt =
-      NoStmt
+      NoStmt of string
     | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     | Datatype of string * (vname list *
         ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
@@ -81,7 +81,7 @@
         inst_params: ((string * (const * int)) * (thm * bool)) list,
         superinst_params: ((string * (const * int)) * (thm * bool)) list };
   type program = stmt Graph.T
-  val empty_funs: program -> string list
+  val unimplemented: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_constr: program -> string -> bool
@@ -419,7 +419,7 @@
 
 type typscheme = (vname * sort) list * itype;
 datatype stmt =
-    NoStmt
+    NoStmt of string
   | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
   | Datatype of string * (vname list * ((string * vname list) * itype list) list)
   | Datatypecons of string * string
@@ -433,8 +433,8 @@
 
 type program = stmt Graph.T;
 
-fun empty_funs program =
-  Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];
+fun unimplemented program =
+  Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program [];
 
 fun map_terms_bottom_up f (t as IConst _) = f t
   | map_terms_bottom_up f (t as IVar _) = f t
@@ -450,7 +450,7 @@
 fun map_classparam_instances_as_term f =
   (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
 
-fun map_terms_stmt f NoStmt = NoStmt
+fun map_terms_stmt f (NoStmt c) = (NoStmt c)
   | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
       (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
   | map_terms_stmt f (stmt as Datatype _) = stmt
@@ -546,7 +546,7 @@
       |> pair name
     else
       program
-      |> Graph.default_node (name, NoStmt)
+      |> Graph.default_node (name, NoStmt "")
       |> add_dep name
       |> pair naming'
       |> curry generate (SOME name)
@@ -651,17 +651,20 @@
     fun stmt_classparam class =
       ensure_class thy algbr eqngr permissive class
       #>> (fn class => Classparam (c, class));
-    fun stmt_fun cert =
-      let
-        val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
-        val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
-        val some_case_cong = Code.get_case_cong thy c;
-      in
-        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
-        ##>> translate_typ thy algbr eqngr permissive ty
-        ##>> translate_eqns thy algbr eqngr permissive eqns'
-        #>> (fn info => Fun (c, (info, some_case_cong)))
-      end;
+    fun stmt_fun cert = case Code.equations_of_cert thy cert
+     of (_, NONE) => pair (NoStmt c)
+      | ((vs, ty), SOME eqns) =>
+          let
+            val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
+            val some_case_cong = Code.get_case_cong thy c;
+          in
+            fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+            ##>> translate_typ thy algbr eqngr permissive ty
+            ##>> translate_eqns thy algbr eqngr permissive eqns'
+            #>>
+             (fn (_, NONE) => NoStmt c
+               | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong)))
+          end;
     val stmt_const = case Code.get_type_of_constr_or_abstr thy c
      of SOME (tyco, _) => stmt_datatypecons tyco
       | NONE => (case Axclass.class_of_param thy c
@@ -762,7 +765,6 @@
   #>> rpair (some_thm, proper)
 and translate_eqns thy algbr eqngr permissive eqns =
   maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
-  #>> these
 and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
   let
     val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
diff -r 6edabf38d929 -r 4121d64fde90 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Tools/nbe.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -415,7 +415,9 @@
   IConst { name = c, typargs = [], dicts = dss,
     dom = [], range = ITyVar "", annotate = false };
 
-fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
+fun eqns_of_stmt (_, Code_Thingol.NoStmt _) =
+      []
+  | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
       []
   | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
       [(const, (vs, map fst eqns))]
@@ -519,7 +521,8 @@
       | is_dict (DFree _) = true
       | is_dict _ = false;
     fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
-     of Code_Thingol.Fun (c, _) => c
+     of Code_Thingol.NoStmt c => c
+      | Code_Thingol.Fun (c, _) => c
       | Code_Thingol.Datatypecons (c, _) => c
       | Code_Thingol.Classparam (c, _) => c);
     fun of_apps bounds (t, ts) =