--- a/src/HOL/Library/Efficient_Nat.thy Mon May 11 09:40:39 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon May 11 10:53:19 2009 +0200
@@ -179,10 +179,8 @@
else NONE
end;
-fun eqn_suc_preproc thy = map fst
- #> gen_eqn_suc_preproc
- @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
- #> (Option.map o map) (Code_Unit.mk_eqn thy);
+val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
+ @{thm Suc_if_eq} I (fst o Logic.dest_equals));
fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
@{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
--- a/src/HOL/Tools/recfun_codegen.ML Mon May 11 09:40:39 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon May 11 10:53:19 2009 +0200
@@ -25,13 +25,13 @@
fun add_thm NONE thm thy = Code.add_eqn thm thy
| add_thm (SOME module_name) thm thy =
- case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
- of SOME (thm', _) => let val c = Code_Unit.const_eqn thy thm'
- in thy
- |> ModuleData.map (Symtab.update (c, module_name))
- |> Code.add_eqn thm'
- end
- | NONE => Code.add_eqn thm thy;
+ let
+ val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true)
+ in
+ thy
+ |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name))
+ |> Code.add_eqn thm'
+ end;
fun meta_eq_to_obj_eq thy thm =
let
--- a/src/HOL/Tools/typecopy_package.ML Mon May 11 09:40:39 2009 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Mon May 11 10:53:19 2009 +0200
@@ -150,7 +150,7 @@
THEN ALLGOALS (rtac @{thm refl})) def_thm)
|-> (fn def_thm => Code.add_eqn def_thm)
|> `(fn thy => mk_eq_refl thy)
- |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
+ |-> (fn refl_thm => Code.add_nbe_eqn refl_thm)
end;
val setup =
--- a/src/Pure/Isar/code.ML Mon May 11 09:40:39 2009 +0200
+++ b/src/Pure/Isar/code.ML Mon May 11 10:53:19 2009 +0200
@@ -20,6 +20,8 @@
val add_inline: thm -> theory -> theory
val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
val del_functrans: string -> theory -> theory
+ val simple_functrans: (theory -> thm list -> thm list option)
+ -> theory -> (thm * bool) list -> (thm * bool) list option
val add_datatype: (string * typ) list -> theory -> theory
val add_datatype_cmd: string list -> theory -> theory
val type_interpretation:
@@ -456,16 +458,6 @@
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in map (Thm.instantiate (instT, [])) thms' end;
-fun check_proper (eqn as (thm, proper)) =
- if proper then eqn else Code_Unit.bad_thm
- ("Duplicate variables on left hand side of code equation:\n"
- ^ Display.string_of_thm thm);
-
-fun mk_eqn thy proper =
- Code_Unit.error_thm ((if proper then check_proper else I) o Code_Unit.mk_eqn thy);
-fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy);
-fun mk_default_eqn thy = Code_Unit.try_thm (check_proper o Code_Unit.mk_eqn thy);
-
(** interfaces and attributes **)
@@ -489,50 +481,44 @@
fun is_constr thy = is_some o get_datatype_of_constr thy;
-fun recheck_eqn thy = Code_Unit.error_thm
- (Code_Unit.assert_linear (is_constr thy) o apfst (Code_Unit.assert_eqn thy));
+fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy);
-fun recheck_eqns_const thy c eqns =
+fun assert_eqns_const thy c eqns =
let
fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm
then eqn else error ("Wrong head of code equation,\nexpected constant "
^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
- in map (cert o recheck_eqn thy) eqns end;
+ in map (cert o assert_eqn thy) eqns end;
fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
o apfst) (fn (_, eqns) => (true, f eqns));
-fun gen_add_eqn proper default thm thy =
- case (if default then mk_default_eqn thy else SOME o mk_eqn thy proper) thm
- of SOME (thm, _) =>
- let
- val c = Code_Unit.const_eqn thy thm;
- val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
- then error ("Rejected polymorphic code equation for overloaded constant:\n"
- ^ Display.string_of_thm thm)
- else ();
- val _ = if not default andalso is_constr thy c
- then error ("Rejected code equation for datatype constructor:\n"
- ^ Display.string_of_thm thm)
- else ();
- in change_eqns false c (add_thm thy default (thm, proper)) thy end
+fun gen_add_eqn default (eqn as (thm, _)) thy =
+ let val c = Code_Unit.const_eqn thy thm
+ in change_eqns false c (add_thm thy default eqn) thy end;
+
+fun add_eqn thm thy =
+ gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy;
+
+fun add_default_eqn thm thy =
+ case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
+ of SOME eqn => gen_add_eqn true eqn thy
| NONE => thy;
-val add_eqn = gen_add_eqn true false;
-val add_default_eqn = gen_add_eqn true true;
-val add_nbe_eqn = gen_add_eqn false false;
+fun add_nbe_eqn thm thy =
+ gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy;
fun add_eqnl (c, lthms) thy =
let
- val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
+ val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
in change_eqns false c (add_lthms lthms') thy end;
val add_default_eqn_attribute = Thm.declaration_attribute
(fn thm => Context.mapping (add_default_eqn thm) I);
val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
-fun del_eqn thm thy = case mk_syntactic_eqn thy thm
+fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
@@ -598,6 +584,10 @@
(map_exec_purge NONE o map_thmproc o apsnd)
(delete_force "function transformer" name);
+fun simple_functrans f thy eqns = case f thy (map fst eqns)
+ of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
+ | NONE => NONE;
+
val _ = Context.>> (Context.map_theory
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
@@ -623,7 +613,7 @@
| apply_functrans thy c [] eqns = eqns
| apply_functrans thy c functrans eqns = eqns
|> perhaps (perhaps_loop (perhaps_apply functrans))
- |> recheck_eqns_const thy c;
+ |> assert_eqns_const thy c;
fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
@@ -644,7 +634,7 @@
|> apply_functrans thy c functrans
|> (map o apfst) (Code_Unit.rewrite_eqn pre)
|> (map o apfst) (AxClass.unoverload thy)
- |> map (recheck_eqn thy)
+ |> map (assert_eqn thy)
|> burrow_fst (common_typ_eqns thy)
end;
--- a/src/Pure/Isar/code_unit.ML Mon May 11 09:40:39 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML Mon May 11 10:53:19 2009 +0200
@@ -6,12 +6,6 @@
signature CODE_UNIT =
sig
- (*generic non-sense*)
- val bad_thm: string -> 'a
- val error_thm: ('a -> 'b) -> 'a -> 'b
- val warning_thm: ('a -> 'b) -> 'a -> 'b option
- val try_thm: ('a -> 'b) -> 'a -> 'b option
-
(*typ instantiations*)
val typscheme: theory -> string * typ -> (string * sort) list * typ
val inst_thm: theory -> sort Vartab.table -> thm -> thm
@@ -35,11 +29,11 @@
-> string * ((string * sort) list * (string * typ list) list)
(*code equations*)
- val assert_eqn: theory -> thm -> thm
- val mk_eqn: theory -> thm -> thm * bool
- val assert_linear: (string -> bool) -> thm * bool -> thm * bool
+ val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
+ val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
+ val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
val const_eqn: theory -> thm -> string
- val const_typ_eqn: thm -> string * typ
+ val const_typ_eqn: thm -> string * typ
val typscheme_eqn: theory -> thm -> (string * sort) list * typ
val expand_eta: theory -> int -> thm -> thm
val rewrite_eqn: simpset -> thm -> thm
@@ -57,13 +51,6 @@
(* auxiliary *)
-exception BAD_THM of string;
-fun bad_thm msg = raise BAD_THM msg;
-fun error_thm f thm = f thm handle BAD_THM msg => error msg;
-fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
- => (warning ("code generator: " ^ msg); NONE);
-fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
-
fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
@@ -323,39 +310,50 @@
(* code equations *)
-fun assert_eqn thy thm =
+exception BAD_THM of string;
+fun bad_thm msg = raise BAD_THM msg;
+fun error_thm f thm = f thm handle BAD_THM msg => error msg;
+fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
+
+fun is_linear thm =
+ let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
+ in not (has_duplicates (op =) ((fold o fold_aterms)
+ (fn Var (v, _) => cons v | _ => I) args [])) end;
+
+fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
- | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+ | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
- | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+ | Free _ => bad_thm ("Illegal free variable in equation\n"
^ Display.string_of_thm thm)
| _ => I) t [];
fun tvars_of t = fold_term_types (fn _ =>
fold_atyps (fn TVar (v, _) => insert (op =) v
| TFree _ => bad_thm
- ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
+ ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
val rhs_tvs = tvars_of rhs;
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
- else bad_thm ("Free variables on right hand side of rewrite theorem\n"
+ else bad_thm ("Free variables on right hand side of equation\n"
^ Display.string_of_thm thm);
val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
then ()
- else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
+ else bad_thm ("Free type variables on right hand side of equation\n"
^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
- val (c, ty) = case head of Const c_ty => c_ty | _ =>
- bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
+ val (c, ty) = case head
+ of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
+ | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
fun check _ (Abs _) = bad_thm
("Abstraction on left hand side of equation\n"
^ Display.string_of_thm thm)
| check 0 (Var _) = ()
| check _ (Var _) = bad_thm
- ("Variable with application on left hand side of code equation\n"
+ ("Variable with application on left hand side of equation\n"
^ Display.string_of_thm thm)
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
@@ -364,44 +362,44 @@
^ Display.string_of_thm thm)
else ();
val _ = map (check 0) args;
+ val _ = (map o map_aterms) (fn t as Const (c, _) => if is_constr_pat c then t
+ else bad_thm (quote c ^ "is not a constructor, on left hand side of equation\n"
+ ^ Display.string_of_thm thm)
+ | t => t) args;
+ val _ = if not proper orelse is_linear thm then ()
+ else bad_thm ("Duplicate variables on left hand side of equation\n"
+ ^ Display.string_of_thm thm);
+ val _ = if (is_none o AxClass.class_of_param thy) c
+ then ()
+ else bad_thm ("Polymorphic constant as head in equation\n"
+ ^ Display.string_of_thm thm)
+ val _ = if not (is_constr_head c)
+ then ()
+ else bad_thm ("Constructor as head in equation\n"
+ ^ Display.string_of_thm thm)
val ty_decl = Sign.the_const_type thy c;
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then () else bad_thm ("Type\n" ^ string_of_typ thy ty
- ^ "\nof code equation\n"
+ ^ "\nof equation\n"
^ Display.string_of_thm thm
^ "\nis incompatible with declared function type\n"
^ string_of_typ thy ty_decl)
- in thm end;
-
-fun add_linear thm =
- let
- val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
- val linear = not (has_duplicates (op =)
- ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
- in (thm, linear) end;
+ in (thm, proper) end;
-fun assert_pat is_cons thm =
- let
- val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
- val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
- else bad_thm ("Not a constructor on left hand side of equation: "
- ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
- | t => t) args;
- in thm end;
-
-fun assert_linear is_cons (thm, false) = (thm, false)
- | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm))
- then (thm, true)
- else bad_thm
- ("Duplicate variables on left hand side of code equation:\n"
- ^ Display.string_of_thm thm);
+fun assert_eqn thy is_constr = gen_assert_eqn thy is_constr is_constr;
val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
fun typscheme_eqn thy = typscheme thy o const_typ_eqn;
-(*permissive wrt. to overloaded constants!*)
-fun mk_eqn thy = add_linear o assert_eqn thy o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+(*these are permissive wrt. to overloaded constants!*)
+fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
+ apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
+
+fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
+ o try_thm (gen_assert_eqn thy is_constr_head (K true))
+ o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+
fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn;