# HG changeset patch
# User haftmann
# Date 1174402361 -3600
# Node ID 25dfebd7b4c873b026c3ee261d4f8415b75af3df
# Parent  86064f2f2188ac6beb645549be170daa03550f51
improved treatment of defining equations stemming from specification tools

diff -r 86064f2f2188 -r 25dfebd7b4c8 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:40 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:41 2007 +0100
@@ -46,7 +46,7 @@
       handle TERM _ => tap (fn _ => warn thm);
   in
     Thm.declaration_attribute (fn thm => Context.mapping
-      (add thm #> CodegenData.add_func_legacy thm) I)
+      (add thm #> CodegenData.add_func false thm) I)
   end;
 
 fun del_thm thm thy =
diff -r 86064f2f2188 -r 25dfebd7b4c8 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Tue Mar 20 15:52:40 2007 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Tue Mar 20 15:52:41 2007 +0100
@@ -145,7 +145,7 @@
 (* hook for projection function code *)
 
 fun add_project (_ , {proj_def, ...} : info) =
-  CodegenData.add_func proj_def;
+  CodegenData.add_func true proj_def;
 
 val setup =
   TypecopyData.init
diff -r 86064f2f2188 -r 25dfebd7b4c8 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Tue Mar 20 15:52:40 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Tue Mar 20 15:52:41 2007 +0100
@@ -11,8 +11,7 @@
   val lazy: (unit -> thm list) -> thm list Susp.T
   val eval_always: bool ref
 
-  val add_func: thm -> theory -> theory
-  val add_func_legacy: thm -> theory -> theory
+  val add_func: bool -> thm -> theory -> theory
   val del_func: thm -> theory -> theory
   val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
   val add_datatype: string * ((string * sort) list * (string * typ list) list)
@@ -515,11 +514,11 @@
 val classop_weakest_typ = gen_classop_typ weakest_constraints;
 val classop_strongest_typ = gen_classop_typ strongest_constraints;
 
-fun gen_mk_func_typ strict_functyp thm =
+fun gen_mk_func_typ strict thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val raw_funcs = CodegenFunc.mk_func thm;
-    val error_warning = if strict_functyp then error else warning #> K NONE;
+    val raw_funcs = CodegenFunc.mk_func strict thm;
+    val error_warning = if strict then error else warning #> K NONE;
     fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) =
           let
             val ((_, ty), _) = CodegenFunc.dest_func thm;
@@ -550,8 +549,7 @@
               ^ CodegenConsts.string_of_typ thy ty_strongest)
           end
       | check_typ_classop class ((c, [_]), thm) =
-          (if strict_functyp then error else warning #> K NONE)
-           ("Illegal type for class operation " ^ quote c
+          error_warning ("Illegal type for class operation " ^ quote c
            ^ "\nin defining equation\n"
            ^ string_of_thm thm);
     fun check_typ_fun (const as (c, _), thm) =
@@ -578,9 +576,9 @@
 
 (** interfaces **)
 
-fun gen_add_func strict_functyp thm thy =
+fun add_func strict thm thy =
   let
-    val funcs = gen_mk_func_typ strict_functyp thm;
+    val funcs = gen_mk_func_typ strict thm;
     val cs = map fst funcs;
   in
     map_exec_purge (SOME cs) (map_funcs 
@@ -592,9 +590,6 @@
   if AList.defined (op =) xs key then AList.delete (op =) key xs
   else error ("No such " ^ msg ^ ": " ^ quote key);
 
-val add_func = gen_add_func true;
-val add_func_legacy = gen_add_func false;
-
 fun del_func thm thy =
   let
     val funcs = gen_mk_func_typ false thm;
@@ -608,7 +603,7 @@
 fun add_funcl (c, lthms) thy =
   let
     val c' = CodegenConsts.norm thy c;
-    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func)) lthms;
+    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func true)) lthms;
   in
     map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
       (add_lthms lthms'))) thy
@@ -835,7 +830,7 @@
       (fn th => Context.mapping (f th) I);
 in
   val _ = map (Context.add_setup o add_simple_attribute) [
-    ("func", add_func),
+    ("func", add_func true),
     ("nofunc", del_func),
     ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
     ("inline", add_inline),
diff -r 86064f2f2188 -r 25dfebd7b4c8 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:40 2007 +0100
+++ b/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:41 2007 +0100
@@ -9,8 +9,8 @@
 sig
   val assert_rew: thm -> thm
   val mk_rew: thm -> thm list
-  val assert_func: thm -> thm
-  val mk_func: thm -> (CodegenConsts.const * thm) list
+  val assert_func: bool -> thm -> thm option
+  val mk_func: bool -> thm -> (CodegenConsts.const * thm) list
   val mk_head: thm -> CodegenConsts.const * thm
   val dest_func: thm -> (string * typ) * term list
   val typ_func: thm -> typ
@@ -77,8 +77,18 @@
 val mk_head = lift_thm_thy (fn thy => fn thm =>
   ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
 
-fun assert_func thm = case try dest_func thm
- of SOME (c_ty as (c, ty), args) =>
+local
+
+exception BAD of string;
+
+fun handle_bad strict thm msg =
+  if strict then error (msg ^ ": " ^ string_of_thm thm)
+    else (warning (msg ^ ": " ^ string_of_thm thm); NONE);
+
+in
+
+fun assert_func strict thm = case try dest_func thm
+ of SOME (c_ty as (c, ty), args) => (
       let
         val thy = Thm.theory_of_thm thm;
         val _ =
@@ -86,23 +96,25 @@
             ((fold o fold_aterms) (fn Var (v, _) => cons v
               | _ => I
             ) args [])
-          then bad_thm "Repeated variables on left hand side of defining equation" thm
+          then raise BAD "Repeated variables on left hand side of defining equation"
           else ()
-        fun check _ (Abs _) = bad_thm
-              "Abstraction on left hand side of defining equation" thm
+        fun check _ (Abs _) = raise BAD
+              "Abstraction on left hand side of defining equation"
           | check 0 (Var _) = ()
-          | check _ (Var _) = bad_thm
-              "Variable with application on left hand side of defining equation" thm
+          | check _ (Var _) = raise BAD
+              "Variable with application on left hand side of defining equation"
           | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
           | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
-              then bad_thm
-                ("Partially applied constant on left hand side of defining equation") thm
+              then raise BAD
+                ("Partially applied constant on left hand side of defining equation")
               else ();
         val _ = map (check 0) args;
-      in thm end
-  | NONE => bad_thm "Not a defining equation" thm;
+      in SOME thm end handle BAD msg => handle_bad strict thm msg)
+  | NONE => handle_bad strict thm "Not a defining equation";
 
-val mk_func = map (mk_head o assert_func) o mk_rew;
+end;
+
+fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew;
 
 
 (* utilities *)