# HG changeset patch
# User panny
# Date 1394762040 -3600
# Node ID 52e8f110fec35a414acb1a60cf5d44116f17184e
# Parent  04c37dfef6847157578f12235463091ae97863cb
print warning if some constructors are missing;
make this warning optional via "(nonexhaustive)"

diff -r 04c37dfef684 -r 52e8f110fec3 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Mar 14 01:28:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Mar 14 02:54:00 2014 +0100
@@ -8,6 +8,8 @@
 
 signature BNF_LFP_REC_SUGAR =
 sig
+  datatype primrec_option = Nonexhaustive_Option
+
   type basic_lfp_sugar =
     {T: typ,
      fp_res_index: int,
@@ -33,7 +35,7 @@
 
   val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
-  val add_primrec_cmd: (binding * string option * mixfix) list ->
+  val add_primrec_cmd: primrec_option list -> (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
@@ -62,6 +64,8 @@
 exception OLD_PRIMREC of unit;
 exception PRIMREC of string * term list;
 
+datatype primrec_option = Nonexhaustive_Option;
+
 datatype rec_call =
   No_Rec of int * typ |
   Mutual_Rec of (int * typ) * (int * typ) |
@@ -346,7 +350,8 @@
       |> fold_rev lambda (args @ left_args @ right_args)
     end);
 
-fun build_defs lthy bs mxs (funs_data : eqn_data list list) (rec_specs : rec_spec list) has_call =
+fun build_defs lthy nonexhaustive bs mxs (funs_data : eqn_data list list)
+    (rec_specs : rec_spec list) has_call =
   let
     val n_funs = length funs_data;
 
@@ -355,8 +360,10 @@
       |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
           ##> (fn x => null x orelse
             raise PRIMREC ("excess equations in definition", map #rhs_term x)) #> fst);
-    val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse
-      raise PRIMREC ("multiple equations for constructor", map #user_eqn x));
+    val _ = ctr_spec_eqn_data_list' |> map (fn ({ctr, ...}, x) =>
+        if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
+        else if length x = 1 orelse nonexhaustive then ()
+        else warning ("no equation for constructor " ^ Syntax.string_of_term lthy ctr));
 
     val ctr_spec_eqn_data_list =
       ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
@@ -414,7 +421,7 @@
   unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN
   HEADGOAL (rtac refl);
 
-fun prepare_primrec fixes specs lthy0 =
+fun prepare_primrec nonexhaustive fixes specs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -455,7 +462,7 @@
         raise PRIMREC ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
           " is not a constructor in left-hand side", [user_eqn])) eqns_data;
 
-    val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
+    val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
 
     fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
         (fun_data : eqn_data list) =
@@ -505,9 +512,10 @@
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
-fun add_primrec_simple fixes ts lthy =
+fun add_primrec_simple' opts fixes ts lthy =
   let
-    val (((names, defs), prove), lthy') = prepare_primrec fixes ts lthy
+    val nonexhaustive = member (op =) opts Nonexhaustive_Option;
+    val (((names, defs), prove), lthy') = prepare_primrec nonexhaustive fixes ts lthy
       handle ERROR str => raise PRIMREC (str, []);
   in
     lthy'
@@ -521,8 +529,10 @@
            error ("primrec error:\n  " ^ str ^ "\nin\n  " ^
              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
 
-fun gen_primrec old_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec
-    lthy =
+val add_primrec_simple = add_primrec_simple' [];
+
+fun gen_primrec old_primrec prep_spec opts
+    (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
   let
     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
@@ -543,7 +553,7 @@
         end);
   in
     lthy
-    |> add_primrec_simple fixes (map snd specs)
+    |> add_primrec_simple' opts fixes (map snd specs)
     |-> (fn (names, (ts, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names simpss)
@@ -551,7 +561,7 @@
   end
   handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
 
-val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec;
+val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
 
 fun add_primrec_global fixes specs =
@@ -564,8 +574,14 @@
   #> add_primrec fixes specs
   ##> Local_Theory.exit_global;
 
+val primrec_option_parser = Parse.group (fn () => "option")
+  (Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option)
+
 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   "define primitive recursive functions"
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd));
+  ((Scan.optional (@{keyword "("} |--
+      Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
+    (Parse.fixes -- Parse_Spec.where_alt_specs)
+    >> (fn (opts, (fixes, spec)) => snd o add_primrec_cmd opts fixes spec));
 
 end;