--- a/src/HOL/Integ/NatBin.thy Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Mon Oct 02 23:00:51 2006 +0200
@@ -790,7 +790,7 @@
val nat_number_expand = thms "nat_number_expand";
-fun elim_number_of_nat thy thms =
+fun elim_number_of_nat thy ts =
let
fun bins_of (Const _) =
I
@@ -809,22 +809,19 @@
| (t', ts) => bins_of t' #> fold bins_of ts;
val simpset =
HOL_basic_ss addsimps nat_number_expand;
- val rewrites =
- []
- |> (fold o Drule.fold_terms) bins_of thms
- |> map (Simplifier.rewrite simpset o Thm.cterm_of thy);
- in if null rewrites then thms else
- map (CodegenData.rewrite_func rewrites) thms
+ in
+ []
+ |> fold (bins_of o Thm.term_of) ts
+ |> map (Simplifier.rewrite simpset o Thm.cterm_of thy)
end;
end;
*}
setup {*
- CodegenData.add_preproc NumeralNat.elim_number_of_nat
+ CodegenData.add_inline_proc NumeralNat.elim_number_of_nat
*}
-
subsection {* legacy ML bindings *}
ML
--- a/src/HOL/OperationalEquality.thy Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/OperationalEquality.thy Mon Oct 02 23:00:51 2006 +0200
@@ -18,17 +18,6 @@
defs
eq_def: "eq x y \<equiv> (x = y)"
-ML {*
-local
- val thy = the_context ();
- val const_eq = Sign.intern_const thy "eq";
- val type_bool = Type (Sign.intern_type thy "bool", []);
-in
- val eq_def_sym = Thm.symmetric (thm "eq_def");
- val class_eq = Sign.intern_class thy "eq";
-end
-*}
-
subsection {* bool type *}
@@ -47,31 +36,24 @@
"eq p False = (\<not> p)" unfolding eq_def by auto
-subsection {* preprocessor *}
+subsection {* code generator setup *}
-ML {*
-fun constrain_op_eq thy thms =
- let
- fun add_eq (Const ("op =", ty)) =
- fold (insert (eq_fst (op = : indexname * indexname -> bool)))
- (Term.add_tvarsT ty [])
- | add_eq _ =
- I
- val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
- val instT = map (fn (v_i, sort) =>
- (Thm.ctyp_of thy (TVar (v_i, sort)),
- Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
- in
- thms
- |> map (Thm.instantiate (instT, []))
- end;
-*}
-
-
-subsection {* codegenerator setup *}
+subsubsection {* preprocessor *}
setup {*
- CodegenData.add_preproc constrain_op_eq
+let
+ val class_eq = "OperationalEquality.eq";
+ fun constrain_op_eq thy ts =
+ let
+ fun add_eq (Const ("op =", ty)) =
+ fold (insert (eq_fst (op = : indexname * indexname -> bool)))
+ (Term.add_tvarsT ty [])
+ | add_eq _ =
+ I
+ val eqs = (fold o fold_aterms) add_eq ts [];
+ val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
+ in inst end;
+in CodegenData.add_constrains constrain_op_eq end
*}
declare eq_def [symmetric, code inline]
--- a/src/HOL/Tools/datatype_codegen.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Mon Oct 02 23:00:51 2006 +0200
@@ -9,10 +9,8 @@
sig
val get_eq: theory -> string -> thm list
val get_eq_datatype: theory -> string -> thm list
- val get_eq_typecopy: theory -> string -> thm list
val get_cert: theory -> bool * string -> thm list
val get_cert_datatype: theory -> string -> thm list
- val get_cert_typecopy: theory -> string -> thm list
val dest_case_expr: theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
val add_datatype_case_const: string -> theory -> theory
@@ -29,11 +27,13 @@
val get_codetypes_arities: theory -> (string * bool) list -> sort
-> (string * (((string * sort list) * sort) * term list)) list option
val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
- -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
- -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
+ -> (((string * sort list) * sort) list -> (string * term list) list -> theory
+ -> ((bstring * attribute list) * term) list * theory)
+ -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
+ -> theory -> theory
val setup: theory -> theory
- val setup2: theory -> theory
+ val setup_hooks: theory -> theory
end;
structure DatatypeCodegen : DATATYPE_CODEGEN =
@@ -364,7 +364,7 @@
val names = Name.invents ctxt "a" (length tys);
val ctxt' = fold Name.declare names ctxt;
val vs = map2 (curry Free) names tys;
- in (vs, ctxt) end;
+ in (vs, ctxt') end;
fun mk_dist ((co1, tys1), (co2, tys2)) =
let
val ((xs1, xs2), _) = Name.context
@@ -400,17 +400,39 @@
|> map (fn t => Goal.prove_global thy [] [] t (K tac))
|> map (fn thm => not_eq_quodlibet OF [thm])
in inject @ distinct end
-and get_cert_typecopy thy dtco =
- let
- val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
- val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
- in
- [thm]
- end;
end (*local*);
-fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
- | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
+local
+ val not_sym = thm "HOL.not_sym";
+ val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+in fun get_eq_datatype thy dtco =
+ let
+ val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
+ fun mk_triv_inject co =
+ let
+ val ct' = Thm.cterm_of thy
+ (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
+ val cty' = Thm.ctyp_of_term ct';
+ val refl = Thm.prop_of HOL.refl;
+ val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
+ (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
+ refl NONE;
+ in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+ val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
+ val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
+ val ctxt = Context.init_proof thy;
+ val simpset = Simplifier.context ctxt
+ (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+ val cos = map (fn (co, tys) =>
+ (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
+ val tac = ALLGOALS (simp_tac simpset)
+ THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
+ val distinct =
+ mk_distinct cos
+ |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+ |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
+ in inject1 @ inject2 @ distinct end;
+end (*local*);
fun add_datatype_case_const dtco thy =
let
@@ -429,8 +451,7 @@
(** codetypes for code 2nd generation **)
-type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
- -> theory -> theory;
+(* abstraction over datatypes vs. type copies *)
fun codetypes_dependency thy =
let
@@ -461,23 +482,54 @@
|> map (AList.make (the o AList.lookup (op =) names))
end;
-fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
- (vs, [(constr, [typ])]);
-
fun get_spec thy (dtco, true) =
(the o DatatypePackage.get_datatype_spec thy) dtco
| get_spec thy (tyco, false) =
- (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
+ TypecopyPackage.get_spec thy tyco;
+
+fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
+ | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
-fun add_spec thy (tyco, is_dt) =
- (tyco, (is_dt, get_spec thy (tyco, is_dt)));
+local
+ val eq_def_sym = thm "eq_def" |> Thm.symmetric;
+ val class_eq = "OperationalEquality.eq";
+ fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
+ of SOME _ => get_eq_datatype thy tyco
+ | NONE => [TypecopyPackage.get_eq thy tyco];
+ fun constrain_op_eq_thms thy thms =
+ let
+ fun add_eq (Const ("op =", ty)) =
+ fold (insert (eq_fst (op =)))
+ (Term.add_tvarsT ty [])
+ | add_eq _ =
+ I
+ val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
+ val instT = map (fn (v_i, sort) =>
+ (Thm.ctyp_of thy (TVar (v_i, sort)),
+ Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
+ in
+ thms
+ |> map (Thm.instantiate (instT, []))
+ end;
+in
+ fun get_eq thy tyco =
+ get_eq_thms thy tyco
+ |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
+ |> constrain_op_eq_thms thy
+ |> map (Tactic.rewrite_rule [eq_def_sym])
+end;
+
+type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+ -> theory -> theory;
fun add_codetypes_hook_bootstrap hook thy =
let
+ fun add_spec thy (tyco, is_dt) =
+ (tyco, (is_dt, get_spec thy (tyco, is_dt)));
fun datatype_hook dtcos thy =
hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
- fun typecopy_hook ((tyco, info )) thy =
- hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
+ fun typecopy_hook ((tyco, _)) thy =
+ hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
in
thy
|> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
@@ -498,6 +550,23 @@
val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
+
+(* registering code types in code generator *)
+
+fun codetype_hook specs =
+ let
+ fun add (dtco, (flag, spec)) thy =
+ let
+ fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
+ in
+ CodegenData.add_datatype
+ (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
+ end;
+ in fold add specs end;
+
+
+(* instrumentalizing the sort algebra *)
+
fun get_codetypes_arities thy tycos sort =
let
val algebra = Sign.classes_of thy;
@@ -538,114 +607,35 @@
then NONE else SOME (arity, (tyco, cs)))) insts;
in
thy
- |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
- arities ("", []) (f thy arities css) #> after_qed)
+ |> K ((not o null) arities) ? (
+ f arities css
+ #-> (fn defs =>
+ ClassPackage.prove_instance_arity tac arities ("", []) defs
+ #> after_qed arities css))
end;
+
+(* operational equality *)
+
local
val class_eq = "OperationalEquality.eq";
-in fun add_eq_instance specs =
- prove_codetypes_arities
- (K (ClassPackage.intro_classes_tac []))
- (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [class_eq] ((K o K o K) [])
-end; (*local*)
-
-local
- val not_sym = thm "HOL.not_sym";
- val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-in fun get_eq_datatype thy dtco =
+in fun eq_hook specs =
let
-(* val _ = writeln "01"; *)
- val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
-(* val _ = writeln "02"; *)
- fun mk_triv_inject co =
+ fun add_eq_thms (dtco, (_, (vs, cs))) thy =
let
- val ct' = Thm.cterm_of (Context.check_thy thy)
- (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
- val cty' = Thm.ctyp_of_term ct';
- val refl = Thm.prop_of HOL.refl;
- val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
- (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I)
- refl NONE;
- in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
-(* val _ = writeln "03"; *)
- val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
-(* val _ = writeln "04"; *)
- val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
-(* val _ = writeln "05"; *)
- val ctxt = Context.init_proof (Context.check_thy thy);
-(* val _ = writeln "06"; *)
- val simpset = Simplifier.context ctxt
- (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
-(* val _ = writeln "07"; *)
- val cos = map (fn (co, tys) =>
- (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
- val tac = ALLGOALS (simp_tac simpset)
- THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
-(* val _ = writeln "08"; *)
- val distinct =
- mk_distinct cos
- |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
- |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
-(* val _ = writeln "09"; *)
- in inject1 @ inject2 @ distinct end;
-
-fun get_eq_typecopy thy tyco =
- case TypecopyPackage.get_typecopy_info thy tyco
- of SOME { inject, ... } => [inject]
- | NONE => [];
-
-local
- val lift_not_thm = thm "HOL.Eq_FalseI";
- val lift_thm = thm "HOL.eq_reflection";
- val eq_def_sym = thm "eq_def" |> Thm.symmetric;
- fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
- of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
- | NONE => case TypecopyPackage.get_typecopy_info thy tyco
- of SOME _ => get_eq_typecopy thy tyco
- | NONE => [];
-in
- fun get_eq thy tyco =
- get_eq_thms (Context.check_thy thy) tyco
-(* |> tap (fn _ => writeln "10") *)
- |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
-(* |> tap (fn _ => writeln "11") *)
- |> constrain_op_eq (Context.check_thy thy)
-(* |> tap (fn _ => writeln "12") *)
- |> map (Tactic.rewrite_rule [eq_def_sym])
-(* |> tap (fn _ => writeln "13") *)
-end;
-
-end;
-
-fun add_eq_thms (dtco, (_, (vs, cs))) thy =
- let
- val thy_ref = Theory.self_ref thy;
- val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
- val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
- val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
- in
- CodegenData.add_funcl
- (c, CodegenData.lazy get_thms) thy
- end;
-
-fun codetype_hook dtcos theory =
- let
- fun add (dtco, (flag, spec)) thy =
- let
- fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
+ val thy_ref = Theory.self_ref thy;
+ val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
+ val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
+ val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
in
- CodegenData.add_datatype
- (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
+ CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
end;
in
- theory
- |> fold add dtcos
+ prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
+ (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+ [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
end;
-
-fun eq_hook dtcos =
- add_eq_instance dtcos (fold add_eq_thms dtcos);
+end; (*local*)
@@ -657,7 +647,7 @@
#> DatatypeHooks.add (fold add_datatype_case_const)
#> DatatypeHooks.add (fold add_datatype_case_defs)
-val setup2 =
+val setup_hooks =
add_codetypes_hook_bootstrap codetype_hook
#> add_codetypes_hook_bootstrap eq_hook
--- a/src/HOL/Tools/typecopy_package.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Mon Oct 02 23:00:51 2006 +0200
@@ -19,8 +19,11 @@
-> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_typecopy_info: theory -> string -> info option
- type hook = string * info -> theory -> theory;
- val add_hook: hook -> theory -> theory;
+ type hook = string * info -> theory -> theory
+ val add_hook: hook -> theory -> theory
+ val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
+ val get_cert: theory -> string -> thm
+ val get_eq: theory -> string -> thm
val print: theory -> unit
val setup: theory -> theory
end;
@@ -134,7 +137,28 @@
end; (*local*)
-(* hooks for projection function code *)
+(* equality function equation *)
+
+fun get_eq thy tyco =
+ (#inject o the o get_typecopy_info thy) tyco;
+
+
+(* datatype specification and certificate *)
+
+fun get_spec thy tyco =
+ let
+ val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
+ in (vs, [(constr, [typ])]) end;
+
+local
+ val bool_eq_implies = thm "iffD1";
+ val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
+in fun get_cert thy tyco =
+ Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
+end; (*local*)
+
+
+(* hook for projection function code *)
fun add_project (_ , { proj_def, ...} : info) =
CodegenData.add_func proj_def;
--- a/src/HOL/ex/CodeEval.thy Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy Mon Oct 02 23:00:51 2006 +0200
@@ -39,15 +39,14 @@
setup {*
let
- fun mk thy arities _ =
- maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
- (Type (tyco, map TFree (Name.names Name.context "'a" asorts)))
- |> tap (writeln o Sign.string_of_term thy))]) arities;
+ fun mk arities _ thy =
+ (maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
+ (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
fun tac _ = ClassPackage.intro_classes_tac [];
fun hook specs =
DatatypeCodegen.prove_codetypes_arities tac
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [TypOf.class_typ_of] mk I
+ [TypOf.class_typ_of] mk ((K o K) I)
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
@@ -90,19 +89,27 @@
setup {*
let
- fun mk thy arities css =
+ fun thy_note ((name, atts), thms) =
+ PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+ fun thy_def ((name, atts), t) =
+ PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ fun mk arities css thy =
let
val vs = (Name.names Name.context "'a" o snd o fst o hd) arities;
- val raw_defs = map (TermOf.mk_terms_of_defs vs) css;
- fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs)
- in ClassPackage.assume_arities_thy thy arities mk' end;
+ val defs = map (TermOf.mk_terms_of_defs vs) css;
+ val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
+ in
+ thy
+ |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
+ |> snd
+ end;
fun tac _ = ClassPackage.intro_classes_tac [];
fun hook specs =
if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I
else
DatatypeCodegen.prove_codetypes_arities tac
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [TermOf.class_term_of] mk I
+ [TermOf.class_term_of] ((K o K o pair) []) mk
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
--- a/src/Pure/Tools/codegen_funcgr.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML Mon Oct 02 23:00:51 2006 +0200
@@ -9,9 +9,10 @@
sig
type T;
val mk_funcgr: theory -> CodegenConsts.const list -> (string * typ) list -> T
+ val all_deps_of: T -> CodegenConsts.const list -> CodegenConsts.const list list
val get_funcs: T -> CodegenConsts.const -> thm list
val get_func_typs: T -> (CodegenConsts.const * typ) list
- val preprocess: theory -> thm list -> thm list
+ val normalize: theory -> thm list -> thm list
val print_codethms: theory -> CodegenConsts.const list -> unit
end;
@@ -98,7 +99,7 @@
val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []);
in Thm.instantiate ([], inst) thm end;
-fun preprocess thy thms =
+fun normalize thy thms =
let
fun burrow_thms f [] = []
| burrow_thms f thms =
@@ -110,7 +111,6 @@
#2 (#1 (Variable.import true thms (ProofContext.init thy)));
in
thms
- |> CodegenData.preprocess thy
|> map (abs_norm thy)
|> burrow_thms (
canonical_tvars thy
@@ -119,43 +119,25 @@
)
end;
-fun check_thms c thms =
- let
- fun check_head_lhs thm (lhs, rhs) =
- case strip_comb lhs
- of (Const (c', _), _) => if c' = c then ()
- else error ("Illegal function equation for " ^ quote c
- ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm)
- | _ => error ("Illegal function equation: " ^ Display.string_of_thm thm);
- fun check_vars_lhs thm (lhs, rhs) =
- if has_duplicates (op =)
- (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
- then error ("Repeated variables on left hand side of function equation:"
- ^ Display.string_of_thm thm)
- else ();
- fun check_vars_rhs thm (lhs, rhs) =
- if null (subtract (op =)
- (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
- (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs []))
- then ()
- else error ("Free variables on right hand side of function equation:"
- ^ Display.string_of_thm thm)
- val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms;
- in
- (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts;
- map2 check_vars_rhs thms tts; thms)
- end;
-
(** retrieval **)
fun get_funcs funcgr (c_tys as (c, _)) =
- (check_thms c o these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
+ (these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
fun get_func_typs funcgr =
AList.make (fst o Constgraph.get_node funcgr) (Constgraph.keys funcgr);
+fun all_deps_of funcgr cs =
+ let
+ val conn = Constgraph.strong_conn funcgr;
+ val order = rev conn;
+ in
+ (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
+ |> filter_out null
+ end;
+
local
fun add_things_of thy f (c, thms) =
@@ -234,7 +216,7 @@
|> Constgraph.new_node (c, [])
|> pair (SOME c)
else let
- val thms = preprocess thy (CodegenData.these_funcs thy c);
+ val thms = normalize thy (CodegenData.these_funcs thy c);
val rhs = rhs_of thy (c, thms);
in
auxgr
--- a/src/Pure/Tools/codegen_names.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML Mon Oct 02 23:00:51 2006 +0200
@@ -236,33 +236,7 @@
(* explicit given names with cache update *)
-fun tyco_force (tyco, name) thy =
- let
- val names = NameSpace.unpack name;
- val (prefix, base) = split_last (NameSpace.unpack name);
- val prefix' = purify_prefix prefix;
- val base' = purify_base base;
- val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
- then ()
- else
- error ("Name violates naming conventions: " ^ quote name
- ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
- val names_ref = CodeName.get thy;
- val (Names names) = ! names_ref;
- val (tycotab, tycorev) = #tyco names;
- val _ = if Symtab.defined tycotab tyco
- then error ("Type constructor already named: " ^ quote tyco)
- else ();
- val _ = if Symtab.defined tycorev name
- then error ("Name already given to type constructor: " ^ quote name)
- else ();
- val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
- Symtab.update_new (name, tyco) tycorev)) (Names names);
- in
- thy
- end;
-
-fun const_force (c_tys as (c, _), name) thy =
+fun force get defined upd_names upd errname string_of (x, name) thy =
let
val names = NameSpace.unpack name;
val (prefix, base) = split_last (NameSpace.unpack name);
@@ -275,44 +249,25 @@
^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
val names_ref = CodeName.get thy;
val (Names names) = ! names_ref;
- val (const, constrev) = #const names;
- val _ = if Consttab.defined const c_tys
- then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
+ val (tab, rev) = get names;
+ val _ = if defined tab x
+ then error ("Already named " ^ errname ^ ": " ^ string_of thy x)
else ();
- val _ = if Symtab.defined constrev name
- then error ("Name already given to constant: " ^ quote name)
+ val _ = if Symtab.defined rev name
+ then error ("Name already given to other " ^ errname ^ ": " ^ quote name)
else ();
- val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
- Symtab.update_new (name, c_tys) constrev)) (Names names);
+ val _ = names_ref := upd_names (K (upd (x, name) tab,
+ Symtab.update_new (name, x) rev)) (Names names);
in
thy
end;
-fun instance_force (instance, name) thy =
- let
- val names = NameSpace.unpack name;
- val (prefix, base) = split_last (NameSpace.unpack name);
- val prefix' = purify_prefix prefix;
- val base' = purify_base base;
- val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
- then ()
- else
- error ("Name violates naming conventions: " ^ quote name
- ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
- val names_ref = CodeName.get thy;
- val (Names names) = ! names_ref;
- val (inst, instrev) = #instance names;
- val _ = if Insttab.defined inst instance
- then error ("Instance already named: " ^ quote (fst instance) ^ ", " ^ quote (snd instance))
- else ();
- val _ = if Symtab.defined instrev name
- then error ("Name already given to instance: " ^ quote name)
- else ();
- val _ = names_ref := map_inst (K (Insttab.update_new (instance, name) inst,
- Symtab.update_new (name, instance) instrev)) (Names names);
- in
- thy
- end;
+val tyco_force = force #tyco Symtab.defined map_tyco Symtab.update_new
+ "type constructor" (K quote);
+val instance_force = force #instance Insttab.defined map_inst Insttab.update_new
+ "instance" (fn _ => fn (class, tyco) => quote class ^ ", " ^ quote tyco);
+val const_force = force #const Consttab.defined map_const Consttab.update_new
+ "constant" (quote oo CodegenConsts.string_of_const);
(* naming policies *)
@@ -442,21 +397,21 @@
val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname");
val constnameP =
- OuterSyntax.command constnameK "declare code name for constant" K.thy_decl (
+ OuterSyntax.improper_command constnameK "declare code name for constant" K.thy_decl (
Scan.repeat1 (P.term -- P.name)
>> (fn aliasses =>
Toplevel.theory (fold const_force_e aliasses))
);
val typenameP =
- OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl (
+ OuterSyntax.improper_command typenameK "declare code name for type constructor" K.thy_decl (
Scan.repeat1 (P.xname -- P.name)
>> (fn aliasses =>
Toplevel.theory (fold tyco_force_e aliasses))
);
val instnameP =
- OuterSyntax.command instnameK "declare code name for instance relation" K.thy_decl (
+ OuterSyntax.improper_command instnameK "declare code name for instance relation" K.thy_decl (
Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name)
>> (fn aliasses =>
Toplevel.theory (fold instance_force_e aliasses))
--- a/src/Pure/Tools/codegen_package.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Mon Oct 02 23:00:51 2006 +0200
@@ -16,7 +16,6 @@
type appgen;
val add_appconst: string * appgen -> theory -> theory;
- val appgen_default: appgen;
val appgen_numeral: (theory -> term -> IntInf.int) -> appgen;
val appgen_char: (term -> int option) -> appgen;
val appgen_case: (theory -> term
@@ -101,8 +100,6 @@
| check_strict has_seri x (true, _) =
true;
-fun no_strict (_, targets) = (false, targets);
-
fun ensure_def_class thy algbr funcgr strct cls trns =
let
fun defgen_class thy (algbr as ((proj_sort, _), _)) funcgr strct cls trns =
@@ -114,7 +111,7 @@
val idfs = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
in
trns
- |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
+ |> tracing (fn _ => "trying defgen class declaration for " ^ quote cls)
|> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
|-> (fn (supcls, memtypes) => succeed
@@ -126,7 +123,7 @@
val cls' = CodegenNames.class thy cls;
in
trns
- |> debug_msg (fn _ => "generating class " ^ quote cls)
+ |> tracing (fn _ => "generating class " ^ quote cls)
|> ensure_def (defgen_class thy algbr funcgr strct) true ("generating class " ^ quote cls) cls'
|> pair cls'
end
@@ -140,7 +137,7 @@
(case CodegenData.get_datatype thy dtco
of SOME (vs, cos) =>
trns
- |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
+ |> tracing (fn _ => "trying defgen datatype for " ^ quote dtco)
|> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
||>> fold_map (fn (c, tys) =>
fold_map (exprgen_type thy algbr funcgr strct) tys
@@ -156,7 +153,7 @@
|> fail ("Not a type constructor: " ^ quote dtco)
in
trns
- |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
+ |> tracing (fn _ => "generating type constructor " ^ quote tyco)
|> ensure_def (defgen_datatype thy algbr funcgr strct) strict
("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
@@ -182,7 +179,7 @@
||>> fold_map (exprgen_type thy algbr funcgr strct) tys
|-> (fn (tyco, tys) => pair (tyco `%% tys));
-exception CONSTRAIN of ((string * typ) * typ) * term option;
+exception CONSTRAIN of (string * typ) * typ;
fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
let
@@ -225,7 +222,7 @@
val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
(curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
val _ = if exists not (map (Sign.of_sort thy) insts)
- then raise CONSTRAIN (((c, ty_decl), ty_ctxt), NONE) else ();
+ then raise CONSTRAIN ((c, ty_decl), ty_ctxt) else ();
in
trns
|> fold_map (exprgen_typinst thy algbr funcgr strct) insts
@@ -251,7 +248,7 @@
||>> exprgen_term thy algbr funcgr strct (Const (m, ty));
in
trns
- |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
+ |> tracing (fn _ => "trying defgen class instance for (" ^ quote cls
^ ", " ^ quote tyco ^ ")")
|> ensure_def_class thy algbr funcgr strct class
||>> ensure_def_tyco thy algbr funcgr strct tyco
@@ -266,7 +263,7 @@
val inst = CodegenNames.instance thy (cls, tyco);
in
trns
- |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
+ |> tracing (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
|> ensure_def (defgen_inst thy algbr funcgr strct) true
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
|> pair inst
@@ -277,7 +274,7 @@
case CodegenData.get_datatype_of_constr thy ((the o CodegenNames.const_rev thy) co)
of SOME tyco =>
trns
- |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
+ |> tracing (fn _ => "trying defgen datatype constructor for " ^ quote co)
|> ensure_def_tyco thy algbr funcgr strct tyco
|-> (fn _ => succeed Bot)
| _ =>
@@ -288,7 +285,7 @@
case AxClass.class_of_param thy ((fst o the o CodegenNames.const_rev thy) m)
of SOME class =>
trns
- |> debug_msg (fn _ => "trying defgen class operation for " ^ quote m)
+ |> tracing (fn _ => "trying defgen class operation for " ^ quote m)
|> ensure_def_class thy algbr funcgr strct class
|-> (fn _ => succeed Bot)
| _ =>
@@ -300,28 +297,16 @@
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
- fun dest_eqthm eq_thm =
- let
- val ((t, args), rhs) =
- (apfst strip_comb o Logic.dest_equals o Logic.unvarify o prop_of) eq_thm;
- in case t
- of Const (c', _) => if c' = c then (args, rhs)
- else error ("Illegal function equation for " ^ quote c
- ^ ", actually defining " ^ quote c')
- | _ => error ("Illegal function equation for " ^ quote c)
- end;
+ val dest_eqthm =
+ apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
fun exprgen_eq (args, rhs) trns =
trns
|> fold_map (exprgen_term thy algbr funcgr strct) args
||>> exprgen_term thy algbr funcgr strct rhs;
- fun checkvars (args, rhs) =
- if CodegenThingol.vars_distinct args then (args, rhs)
- else error ("Repeated variables on left hand side of function")
in
trns
|> message msg (fn trns => trns
|> fold_map (exprgen_eq o dest_eqthm) eq_thms
- |-> (fn eqs => pair (map checkvars eqs))
||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
||>> exprgen_type thy algbr funcgr strct ty
|-> (fn ((eqs, vs), ty) => succeed (Fun (eqs, (vs, ty)))))
@@ -342,7 +327,7 @@
val strict = check_strict (CodegenSerializer.const_has_serialization thy) idf strct;
in
trns
- |> debug_msg (fn _ => "generating constant "
+ |> tracing (fn _ => "generating constant "
^ (quote o CodegenConsts.string_of_const thy) (c, tys))
|> ensure_def (get_defgen funcgr strct idf) strict ("generating constant "
^ CodegenConsts.string_of_const thy (c, tys)) idf
@@ -415,24 +400,18 @@
|> appgen_default thy algbr funcgr strct ((f, ty), ts);
-(* entry points into extraction kernel *)
+(* entrance points into extraction kernel *)
fun ensure_def_const' thy algbr funcgr strct c trns =
ensure_def_const thy algbr funcgr strct c trns
- handle CONSTRAIN (((c, ty), ty_decl), NONE) => error (
+ handle CONSTRAIN ((c, ty), ty_decl) => error (
"Constant " ^ c ^ " with most general type\n"
^ Sign.string_of_typ thy ty
^ "\noccurs with type\n"
- ^ Sign.string_of_typ thy ty_decl)
- handle CONSTRAIN (((c, ty), ty_decl), SOME t) => error ("In term " ^ (quote o Sign.string_of_term thy) t
- ^ ",\nconstant " ^ c ^ " with most general type\n"
- ^ Sign.string_of_typ thy ty
- ^ "\noccurs with type\n"
^ Sign.string_of_typ thy ty_decl);
-
fun exprgen_term' thy algbr funcgr strct t trns =
exprgen_term thy algbr funcgr strct t trns
- handle CONSTRAIN (((c, ty), ty_decl), _) => error ("In term " ^ (quote o Sign.string_of_term thy) t
+ handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
^ ",\nconstant " ^ c ^ " with most general type\n"
^ Sign.string_of_typ thy ty
^ "\noccurs with type\n"
@@ -444,16 +423,13 @@
fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
case try (int_of_numeral thy) (list_comb (Const c, ts))
- of SOME i => (*if i < 0 then (*preprocessor eliminates negative numerals*)
+ of SOME i =>
trns
- |> appgen_default thy algbr funcgr (no_strict strct) app
- else*)
- trns
- |> appgen_default thy algbr funcgr (no_strict strct) app
+ |> appgen_default thy algbr funcgr strct app
|-> (fn e => pair (CodegenThingol.INum (i, e)))
| NONE =>
trns
- |> appgen_default thy algbr funcgr (no_strict strct) app;
+ |> appgen_default thy algbr funcgr strct app;
fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns =
case (char_to_index o list_comb o apfst Const) app
@@ -521,9 +497,18 @@
fun codegen_term thy t =
let
+ fun const_typ (c, ty) =
+ let
+ val const = CodegenConsts.norm_of_typ thy (c, ty);
+ val funcgr = CodegenFuncgr.mk_funcgr thy [const] [];
+ in case CodegenFuncgr.get_funcs funcgr const
+ of (thm :: _) => CodegenData.typ_func thy thm
+ | [] => Sign.the_const_type thy c
+ end;
val ct = Thm.cterm_of thy t;
- val thm = CodegenData.preprocess_cterm thy ct;
- val t' = (snd o Logic.dest_equals o Drule.plain_prop_of) thm;
+ val (thm, ct') = CodegenData.preprocess_cterm thy
+ (const_typ) ct;
+ val t' = Thm.term_of ct';
val cs_rhss = CodegenConsts.consts_of thy t';
in
(thm, generate thy cs_rhss (SOME []) NONE exprgen_term' t')
@@ -540,18 +525,7 @@
val _ = Term.fold_atyps (fn _ =>
error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
(Term.fastype_of t);
- fun preprocess_term t =
- let
- val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
- (* fake definition *)
- val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
- (Logic.mk_equals (x, t));
- fun err () = error "preprocess_term: bad preprocessor"
- in case map prop_of (CodegenFuncgr.preprocess thy [eq])
- of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
- | _ => err ()
- end;
- val (_, t') = codegen_term thy (preprocess_term t);
+ val (_, t') = codegen_term thy t;
in
CodegenSerializer.eval_term thy (ref_spec, t') (Code.get thy)
end;
@@ -613,7 +587,7 @@
"code_class", "code_instance", "code_type", "code_const");
val codeP =
- OuterSyntax.command codeK "generate and serialize executable code for constants" K.diag (
+ OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
Scan.repeat P.term
-- Scan.repeat (P.$$$ "(" |--
P.name :-- (fn target => (CodegenSerializer.parse_serializer target >> SOME) || pair NONE)
--- a/src/Pure/Tools/codegen_thingol.ML Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Mon Oct 02 23:00:51 2006 +0200
@@ -95,8 +95,8 @@
val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
val elim_classes: module -> (iterm list * iterm) list * typscheme -> (iterm list * iterm) list * itype;
- val debug: bool ref;
- val debug_msg: ('a -> string) -> 'a -> 'a;
+ val trace: bool ref;
+ val tracing: ('a -> string) -> 'a -> 'a;
val soft_exc: bool ref;
val serialize:
@@ -112,8 +112,8 @@
(** auxiliary **)
-val debug = ref false;
-fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
+val trace = ref false;
+fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
val soft_exc = ref true;
fun unfoldl dest x =
@@ -1057,7 +1057,7 @@
^ (if strict then " (strict)" else " (non-strict)");
fun add_dp NONE = I
| add_dp (SOME dep) =
- debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
+ tracing (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
#> add_dep (dep, name);
fun prep_def def modl =
(check_prep_def modl def, modl);
@@ -1077,22 +1077,22 @@
modl
|> (if can (get_def modl) name
then
- debug_msg (fn _ => "asserting node " ^ quote name)
+ tracing (fn _ => "asserting node " ^ quote name)
#> add_dp dep
else
- debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
+ tracing (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
#> ensure_bot name
#> add_dp dep
- #> debug_msg (fn _ => "creating node " ^ quote name)
+ #> tracing (fn _ => "creating node " ^ quote name)
#> invoke_generator name defgen
#-> (fn def => prep_def def)
#-> (fn def =>
- debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
- #> debug_msg (fn _ => "adding")
+ tracing (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
+ #> tracing (fn _ => "adding")
#> add_def_incr strict (name, def)
- #> debug_msg (fn _ => "postprocessing")
+ #> tracing (fn _ => "postprocessing")
#> postprocess_def (name, def)
- #> debug_msg (fn _ => "adding done")
+ #> tracing (fn _ => "adding done")
))
|> pair dep
end;