1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:40 2007 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:41 2007 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4        handle TERM _ => tap (fn _ => warn thm);
     1.5    in
     1.6      Thm.declaration_attribute (fn thm => Context.mapping
     1.7 -      (add thm #> CodegenData.add_func_legacy thm) I)
     1.8 +      (add thm #> CodegenData.add_func false thm) I)
     1.9    end;
    1.10  
    1.11  fun del_thm thm thy =

     2.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Mar 20 15:52:40 2007 +0100
     2.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Mar 20 15:52:41 2007 +0100
     2.3 @@ -145,7 +145,7 @@
     2.4  (* hook for projection function code *)
     2.5  
     2.6  fun add_project (_ , {proj_def, ...} : info) =
     2.7 -  CodegenData.add_func proj_def;
     2.8 +  CodegenData.add_func true proj_def;
     2.9  
    2.10  val setup =
    2.11    TypecopyData.init

     3.1 --- a/src/Pure/Tools/codegen_data.ML	Tue Mar 20 15:52:40 2007 +0100
     3.2 +++ b/src/Pure/Tools/codegen_data.ML	Tue Mar 20 15:52:41 2007 +0100
     3.3 @@ -11,8 +11,7 @@
     3.4    val lazy: (unit -> thm list) -> thm list Susp.T
     3.5    val eval_always: bool ref
     3.6  
     3.7 -  val add_func: thm -> theory -> theory
     3.8 -  val add_func_legacy: thm -> theory -> theory
     3.9 +  val add_func: bool -> thm -> theory -> theory
    3.10    val del_func: thm -> theory -> theory
    3.11    val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
    3.12    val add_datatype: string * ((string * sort) list * (string * typ list) list)
    3.13 @@ -515,11 +514,11 @@
    3.14  val classop_weakest_typ = gen_classop_typ weakest_constraints;
    3.15  val classop_strongest_typ = gen_classop_typ strongest_constraints;
    3.16  
    3.17 -fun gen_mk_func_typ strict_functyp thm =
    3.18 +fun gen_mk_func_typ strict thm =
    3.19    let
    3.20      val thy = Thm.theory_of_thm thm;
    3.21 -    val raw_funcs = CodegenFunc.mk_func thm;
    3.22 -    val error_warning = if strict_functyp then error else warning #> K NONE;
    3.23 +    val raw_funcs = CodegenFunc.mk_func strict thm;
    3.24 +    val error_warning = if strict then error else warning #> K NONE;
    3.25      fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) =
    3.26            let
    3.27              val ((_, ty), _) = CodegenFunc.dest_func thm;
    3.28 @@ -550,8 +549,7 @@
    3.29                ^ CodegenConsts.string_of_typ thy ty_strongest)
    3.30            end
    3.31        | check_typ_classop class ((c, [_]), thm) =
    3.32 -          (if strict_functyp then error else warning #> K NONE)
    3.33 -           ("Illegal type for class operation " ^ quote c
    3.34 +          error_warning ("Illegal type for class operation " ^ quote c
    3.35             ^ "\nin defining equation\n"
    3.36             ^ string_of_thm thm);
    3.37      fun check_typ_fun (const as (c, _), thm) =
    3.38 @@ -578,9 +576,9 @@
    3.39  
    3.40  (** interfaces **)
    3.41  
    3.42 -fun gen_add_func strict_functyp thm thy =
    3.43 +fun add_func strict thm thy =
    3.44    let
    3.45 -    val funcs = gen_mk_func_typ strict_functyp thm;
    3.46 +    val funcs = gen_mk_func_typ strict thm;
    3.47      val cs = map fst funcs;
    3.48    in
    3.49      map_exec_purge (SOME cs) (map_funcs 
    3.50 @@ -592,9 +590,6 @@
    3.51    if AList.defined (op =) xs key then AList.delete (op =) key xs
    3.52    else error ("No such " ^ msg ^ ": " ^ quote key);
    3.53  
    3.54 -val add_func = gen_add_func true;
    3.55 -val add_func_legacy = gen_add_func false;
    3.56 -
    3.57  fun del_func thm thy =
    3.58    let
    3.59      val funcs = gen_mk_func_typ false thm;
    3.60 @@ -608,7 +603,7 @@
    3.61  fun add_funcl (c, lthms) thy =
    3.62    let
    3.63      val c' = CodegenConsts.norm thy c;
    3.64 -    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func)) lthms;
    3.65 +    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func true)) lthms;
    3.66    in
    3.67      map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
    3.68        (add_lthms lthms'))) thy
    3.69 @@ -835,7 +830,7 @@
    3.70        (fn th => Context.mapping (f th) I);
    3.71  in
    3.72    val _ = map (Context.add_setup o add_simple_attribute) [
    3.73 -    ("func", add_func),
    3.74 +    ("func", add_func true),
    3.75      ("nofunc", del_func),
    3.76      ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
    3.77      ("inline", add_inline),

     4.1 --- a/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:40 2007 +0100
     4.2 +++ b/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:41 2007 +0100
     4.3 @@ -9,8 +9,8 @@
     4.4  sig
     4.5    val assert_rew: thm -> thm
     4.6    val mk_rew: thm -> thm list
     4.7 -  val assert_func: thm -> thm
     4.8 -  val mk_func: thm -> (CodegenConsts.const * thm) list
     4.9 +  val assert_func: bool -> thm -> thm option
    4.10 +  val mk_func: bool -> thm -> (CodegenConsts.const * thm) list
    4.11    val mk_head: thm -> CodegenConsts.const * thm
    4.12    val dest_func: thm -> (string * typ) * term list
    4.13    val typ_func: thm -> typ
    4.14 @@ -77,8 +77,18 @@
    4.15  val mk_head = lift_thm_thy (fn thy => fn thm =>
    4.16    ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
    4.17  
    4.18 -fun assert_func thm = case try dest_func thm
    4.19 - of SOME (c_ty as (c, ty), args) =>
    4.20 +local
    4.21 +
    4.22 +exception BAD of string;
    4.23 +
    4.24 +fun handle_bad strict thm msg =
    4.25 +  if strict then error (msg ^ ": " ^ string_of_thm thm)
    4.26 +    else (warning (msg ^ ": " ^ string_of_thm thm); NONE);
    4.27 +
    4.28 +in
    4.29 +
    4.30 +fun assert_func strict thm = case try dest_func thm
    4.31 + of SOME (c_ty as (c, ty), args) => (
    4.32        let
    4.33          val thy = Thm.theory_of_thm thm;
    4.34          val _ =
    4.35 @@ -86,23 +96,25 @@
    4.36              ((fold o fold_aterms) (fn Var (v, _) => cons v
    4.37                | _ => I
    4.38              ) args [])
    4.39 -          then bad_thm "Repeated variables on left hand side of defining equation" thm
    4.40 +          then raise BAD "Repeated variables on left hand side of defining equation"
    4.41            else ()
    4.42 -        fun check _ (Abs _) = bad_thm
    4.43 -              "Abstraction on left hand side of defining equation" thm
    4.44 +        fun check _ (Abs _) = raise BAD
    4.45 +              "Abstraction on left hand side of defining equation"
    4.46            | check 0 (Var _) = ()
    4.47 -          | check _ (Var _) = bad_thm
    4.48 -              "Variable with application on left hand side of defining equation" thm
    4.49 +          | check _ (Var _) = raise BAD
    4.50 +              "Variable with application on left hand side of defining equation"
    4.51            | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    4.52            | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
    4.53 -              then bad_thm
    4.54 -                ("Partially applied constant on left hand side of defining equation") thm
    4.55 +              then raise BAD
    4.56 +                ("Partially applied constant on left hand side of defining equation")
    4.57                else ();
    4.58          val _ = map (check 0) args;
    4.59 -      in thm end
    4.60 -  | NONE => bad_thm "Not a defining equation" thm;
    4.61 +      in SOME thm end handle BAD msg => handle_bad strict thm msg)
    4.62 +  | NONE => handle_bad strict thm "Not a defining equation";
    4.63  
    4.64 -val mk_func = map (mk_head o assert_func) o mk_rew;
    4.65 +end;
    4.66 +
    4.67 +fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew;
    4.68  
    4.69  
    4.70  (* utilities *)