--- 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 =
--- 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
--- 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),
--- 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 *)