--- a/src/Pure/IsaMakefile Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/IsaMakefile Thu Apr 06 16:08:25 2006 +0200
@@ -59,7 +59,7 @@
Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML \
Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/class_package.ML \
Tools/codegen_thingol.ML Tools/codegen_serializer.ML Tools/codegen_package.ML \
- Tools/am_compiler.ML \
+ Tools/codegen_theorems.ML Tools/am_compiler.ML \
Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML \
Tools/nbe.ML Tools/nbe_eval.ML Tools/nbe_codegen.ML \
codegen.ML compress.ML consts.ML context.ML defs.ML display.ML \
--- a/src/Pure/Tools/ROOT.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML Thu Apr 06 16:08:25 2006 +0200
@@ -7,12 +7,12 @@
(*class package*)
use "class_package.ML";
+(*code generator, 1st generation*)
+use "../codegen.ML";
+
(*code generator theorems*)
use "codegen_theorems.ML";
-(*code generator, 1st generation*)
-use "../codegen.ML";
-
(*code generator, 2nd generation*)
use "codegen_thingol.ML";
use "codegen_serializer.ML";
--- a/src/Pure/Tools/codegen_package.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Thu Apr 06 16:08:25 2006 +0200
@@ -9,18 +9,12 @@
signature CODEGEN_PACKAGE =
sig
type auxtab;
- type eqextr = theory -> auxtab
- -> string * typ -> (thm list * typ) option;
- type eqextr_default = theory -> auxtab
- -> string * typ -> ((thm list * term option) * typ) option;
type appgen = theory -> auxtab
-> (string * typ) * term list -> CodegenThingol.transact
-> CodegenThingol.iexpr * CodegenThingol.transact;
val add_appconst: string * ((int * int) * appgen) -> theory -> theory;
val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory;
- val add_eqextr: string * eqextr -> theory -> theory;
- val add_eqextr_default: string * eqextr_default -> theory -> theory;
val add_prim_class: xstring -> (string * string)
-> theory -> theory;
val add_prim_tyco: xstring -> (string * string)
@@ -55,8 +49,6 @@
val appgen_number_of: (term -> term) -> (theory -> term -> IntInf.int) -> string -> string
-> appgen;
val appgen_wfrec: appgen;
- val eqextr_eq: (theory -> string -> thm list) -> term
- -> eqextr_default;
val add_case_const: (theory -> string -> (string * int) list option) -> xstring
-> theory -> theory;
val add_case_const_i: (theory -> string -> (string * int) list option) -> string
@@ -77,6 +69,7 @@
val alias_get: theory -> string -> string;
val idf_of_name: theory -> string -> string -> string;
val idf_of_const: theory -> auxtab -> string * typ -> string;
+ val idf_of_co: theory -> auxtab -> string * string -> string option;
end;
structure CodegenPackage : CODEGEN_PACKAGE =
@@ -132,7 +125,7 @@
(* code generator basics *)
-type deftab = (typ * (thm * string)) list Symtab.table;
+type deftab = (typ * thm) list Symtab.table;
fun eq_typ thy (ty1, ty2) =
Sign.typ_instance thy (ty1, ty2)
@@ -165,7 +158,7 @@
val prefix =
case (AList.lookup (eq_typ thy)
(Defs.specifications_of (Theory.defs_of thy) c)) ty
- of SOME thyname => NameSpace.append thyname nsp_overl
+ of SOME (_, thyname) => NameSpace.append thyname nsp_overl
| NONE => if c = "op ="
then
NameSpace.append
@@ -368,7 +361,12 @@
logic_data = merge_logic_data (logic_data1, logic_data2),
target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
};
- fun print _ _ = ();
+ fun print thy (data : T) =
+ let
+ val module = #modl data
+ in
+ (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module]
+ end;
end);
val _ = Context.add_setup CodegenData.init;
@@ -381,13 +379,7 @@
in CodegenData.put { modl = modl, gens = gens,
target_data = target_data, logic_data = logic_data } thy end;
-fun print_code thy =
- let
- val module = (#modl o CodegenData.get) thy;
- in
- (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module]
- end;
-
+val print_code = CodegenData.print;
(* advanced name handling *)
@@ -403,7 +395,28 @@
val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get,
perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get);
-fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), dtcontab)))
+fun idf_of_co thy (tabs as (_, (_, _, dtcontab))) (co, dtco) =
+ case CodegenTheorems.get_datatypes thy dtco
+ of SOME ((_, cos), _) => if AList.defined (op =) cos co
+ then try (DatatypeconsNameMangler.get thy dtcontab) (co, dtco)
+ |> the_default co
+ |> idf_of_name thy nsp_dtcon
+ |> SOME
+ else NONE
+ | NONE => NONE;
+
+fun co_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
+ case name_of_idf thy nsp_dtcon idf
+ of SOME idf' => let
+ val (c, dtco) = case try (DatatypeconsNameMangler.rev thy dtcontab) idf'
+ of SOME c_dtco => c_dtco
+ | NONE => case (snd o strip_type o Sign.the_const_type thy) idf'
+ of Type (dtco, _) => (idf', dtco)
+ | _ => (idf', "nat") (*a hack*)
+ in SOME (c, dtco) end
+ | NONE => NONE;
+
+fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), _)))
(c, ty) =
let
fun get_overloaded (c, ty) =
@@ -416,11 +429,10 @@
| _ => NONE)
fun get_datatypecons (c, ty) =
case (snd o strip_type) ty
- of Type (tyco, _) =>
- try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco)
+ of Type (tyco, _) => idf_of_co thy tabs (c, tyco)
| _ => NONE;
in case get_datatypecons (c, ty)
- of SOME c' => idf_of_name thy nsp_dtcon c'
+ of SOME idf => idf
| NONE => case get_overloaded (c, ty)
of SOME idf => idf
| NONE => case ClassPackage.lookup_const_class thy c
@@ -440,16 +452,6 @@
| NONE => NONE
);
-fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
- case recconst_of_idf thy tabs idf
- of SOME c_ty => SOME c_ty
- | NONE => case dest_nsp nsp_mem idf
- of SOME c => SOME (c, Sign.the_const_constraint thy c)
- | NONE => case name_of_idf thy nsp_dtcon idf
- of SOME idf' => let
- val c = (fst o DatatypeconsNameMangler.rev thy dtcontab) idf'
- in SOME (c, Sign.the_const_type thy c) end
- | NONE => NONE;
(* further theory data accessors *)
@@ -469,31 +471,6 @@
val add_appconst = gen_add_appconst Sign.intern_const;
val add_appconst_i = gen_add_appconst (K I);
-fun add_eqextr (name, eqx) =
- map_codegen_data
- (fn (modl, gens, target_data, logic_data) =>
- (modl,
- gens |> map_gens
- (fn (appconst, eqextrs) =>
- (appconst, eqextrs
- |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
- (name, ((Option.map o apfst o rpair) NONE ooo eqx , stamp ())))),
- target_data, logic_data));
-
-fun add_eqextr_default (name, eqx) =
- map_codegen_data
- (fn (modl, gens, target_data, logic_data) =>
- (modl,
- gens |> map_gens
- (fn (appconst, eqextrs) =>
- (appconst, eqextrs
- |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
- (name, (eqx, stamp ())))),
- target_data, logic_data));
-
-fun get_eqextrs thy tabs =
- (map (fn (name, (eqx, _)) => (name, eqx thy tabs)) o #eqextrs o #gens o CodegenData.get) thy;
-
fun set_get_all_datatype_cons f =
map_codegen_data
(fn (modl, gens, target_data, logic_data) =>
@@ -520,6 +497,15 @@
of NONE => K NONE
| SOME (f, _) => f thy;
+fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
+ case recconst_of_idf thy tabs idf
+ of SOME c_ty => SOME c_ty
+ | NONE => case dest_nsp nsp_mem idf
+ of SOME c => SOME (c, Sign.the_const_constraint thy c)
+ | NONE => case co_of_idf thy tabs idf
+ of SOME (c, dtco) => SOME (c, Type (dtco, (the o AList.lookup (op =) ((snd o fst o the o CodegenTheorems.get_datatypes thy) dtco)) c))
+ | NONE => NONE;
+
fun set_int_tyco tyco thy =
(serializers := (
! serializers
@@ -533,75 +519,6 @@
); thy);
-(* sophisticated devarification *)
-
-fun devarify_typs tys =
- let
- fun add_rename (vi as (v, _), sorts) used =
- let
- val v' = "'" ^ variant used (unprefix "'" v)
- in (map (fn sort => (((vi, sort), TFree (v', sort)), (v', TVar (vi, sort)))) sorts, v' :: used) end;
- fun typ_names (Type (tyco, tys)) (vars, names) =
- (vars, names |> insert (op =) (NameSpace.base tyco))
- |> fold typ_names tys
- | typ_names (TFree (v, _)) (vars, names) =
- (vars, names |> insert (op =) (unprefix "'" v))
- | typ_names (TVar (vi, sort)) (vars, names) =
- (vars
- |> AList.default (op =) (vi, [])
- |> AList.map_entry (op =) vi (cons sort),
- names);
- val (vars, used) = fold typ_names tys ([], []);
- val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list;
- in
- (reverse, map (Term.instantiateT renames) tys)
- end;
-
-fun burrow_typs_yield f ts =
- let
- val typtab =
- fold (fold_types (fn ty => Typtab.update (ty, dummyT)))
- ts Typtab.empty;
- val typs = Typtab.keys typtab;
- val (x, typs') = f typs;
- val typtab' = fold2 (Typtab.update oo pair) typs typs' typtab;
- in
- (x, (map o map_term_types) (the o Typtab.lookup typtab') ts)
- end;
-
-fun devarify_terms ts =
- let
- fun add_rename (vi as (v, _), tys) used =
- let
- val v' = variant used v
- in (map (fn ty => (((vi, ty), Free (v', ty)), (v', Var (vi, ty)))) tys, v' :: used) end;
- fun term_names (Const (c, _)) (vars, names) =
- (vars, names |> insert (op =) (NameSpace.base c))
- | term_names (Free (v, _)) (vars, names) =
- (vars, names |> insert (op =) v)
- | term_names (Var (vi, ty)) (vars, names) =
- (vars
- |> AList.default (op =) (vi, [])
- |> AList.map_entry (op =) vi (cons ty),
- names)
- | term_names (Bound _) vars_names =
- vars_names
- | term_names (Abs (v, _, _)) (vars, names) =
- (vars, names |> insert (op =) v)
- | term_names (t1 $ t2) vars_names =
- vars_names |> term_names t1 |> term_names t2
- val (vars, used) = fold term_names ts ([], []);
- val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list;
- in
- (reverse, map (Term.instantiate ([], renames)) ts)
- end;
-
-fun devarify_term_typs ts =
- ts
- |> devarify_terms
- |-> (fn reverse => burrow_typs_yield devarify_typs
- #-> (fn reverseT => pair (reverseT, reverse)));
-
(* definition and expression generators *)
fun ensure_def_class thy tabs cls trns =
@@ -615,7 +532,7 @@
val idfs = map (idf_of_name thy nsp_mem o fst) cs;
in
trns
- |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
+ |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
|> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
||>> (exprsgen_type thy tabs o map snd) cs
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
@@ -628,7 +545,7 @@
val cls' = idf_of_name thy nsp_class cls;
in
trns
- |> debug 4 (fn _ => "generating class " ^ quote cls)
+ |> debug_msg (fn _ => "generating class " ^ quote cls)
|> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
|> pair cls'
end
@@ -637,19 +554,16 @@
fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
case name_of_idf thy nsp_tyco dtco
of SOME dtco =>
- (case get_datatype thy dtco
- of SOME (vars, cos) =>
- let
- val cos' = map (fn (co, tys) => (DatatypeconsNameMangler.get thy dtcontab (co, dtco) |>
- idf_of_name thy nsp_dtcon, tys)) cos;
- in
- trns
- |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
- |> fold_map (exprgen_tyvar_sort thy tabs) vars
- ||>> fold_map (fn (c, ty) => exprsgen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
- |-> (fn (sorts, cos'') => succeed (Datatype
- (sorts, cos'')))
- end
+ (case CodegenTheorems.get_datatypes thy dtco
+ of SOME ((vars, cos), _) =>
+ trns
+ |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
+ |> fold_map (exprgen_tyvar_sort thy tabs) vars
+ ||>> fold_map (fn (c, ty) =>
+ exprsgen_type thy tabs ty
+ #-> (fn ty' => pair ((the o idf_of_co thy tabs) (c, dtco), ty'))) cos
+ |-> (fn (vars, cos) => succeed (Datatype
+ (vars, cos)))
| NONE =>
trns
|> fail ("no datatype found for " ^ quote dtco))
@@ -659,7 +573,7 @@
val tyco' = idf_of_name thy nsp_tyco tyco;
in
trns
- |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
+ |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
|> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
@@ -684,7 +598,7 @@
||>> fold_map (exprgen_type thy tabs) tys
|-> (fn (tyco, tys) => pair (tyco `%% tys))
and exprsgen_type thy tabs =
- fold_map (exprgen_type thy tabs) o snd o devarify_typs;
+ fold_map (exprgen_type thy tabs);
fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
trns
@@ -695,46 +609,28 @@
trns
|> fold_map (ensure_def_class thy tabs) clss
|-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
-and mk_fun thy tabs restrict (c, ty1) trns =
- case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs)
- of SOME ((eq_thms, default), ty2) =>
+and mk_fun thy tabs (c, ty) trns =
+ case CodegenTheorems.get_funs thy (c, Type.varifyT ty)
+ of SOME (ty, eq_thms) =>
let
- val ty3 = if restrict then ty1 else ty2;
- val sortctxt = ClassPackage.extract_sortctxt thy ty3;
- val instantiate = if restrict
- then
- let
- val tab_lookup = snd o the o Vartab.lookup (Sign.typ_match thy (ty2, ty1) Vartab.empty);
- in map_term_types (map_atyps (fn (TVar (vi, _)) => tab_lookup vi
- | ty => ty)) end
- else I
+ val sortctxt = ClassPackage.extract_sortctxt thy ty;
fun dest_eqthm eq_thm =
let
val ((t, args), rhs) =
- (apfst strip_comb o Logic.dest_equals o instantiate
- o prop_of o Drule.zero_var_indexes) eq_thm;
+ (apfst strip_comb o Logic.dest_equals
+ 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;
- fun mk_default t =
- let
- val (tys, ty') = strip_type ty3;
- val vs = Term.invent_names (add_term_names (t, [])) "x" (length tys);
- in
- if (not o eq_typ thy) (type_of t, ty')
- then error ("inconsistent type for default rule")
- else (map2 (curry Free) vs tys, t)
- end;
in
trns
|> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms
- ||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default
- ||>> exprsgen_type thy tabs [ty3]
+ ||>> exprsgen_type thy tabs [ty]
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
- |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) ((eqs @ eq_default, (sortctxt, ty)), ty3))
+ |-> (fn ((eqs, [ity]), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))
end
| NONE => (NONE, trns)
and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
@@ -753,17 +649,16 @@
|-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
fun gen_membr (m, ty) trns =
trns
- |> mk_fun thy tabs true (m, ty)
+ |> mk_fun thy tabs (m, ty)
|-> (fn NONE => error ("could not derive definition for member "
^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
- | SOME (funn, ty_use) =>
- (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup_member thy (ty, ty_use))
+ | SOME (funn, ty_decl) => (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup_member thy (ty_decl, ty))
#-> (fn lss =>
pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
in
trns
- |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls
+ |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
^ ", " ^ quote tyco ^ ")")
|> ensure_def_class thy tabs class
||>> ensure_def_tyco thy tabs tyco
@@ -779,7 +674,7 @@
val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
in
trns
- |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
+ |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
|> ensure_def [("instance", defgen_inst thy tabs)]
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
|> pair inst
@@ -790,7 +685,7 @@
case recconst_of_idf thy tabs c
of SOME (c, ty) =>
trns
- |> mk_fun thy tabs false (c, ty)
+ |> mk_fun thy tabs (c, ty)
|-> (fn SOME (funn, _) => succeed (Fun funn)
| NONE => fail ("no defining equations found for " ^ quote c))
| NONE =>
@@ -800,16 +695,16 @@
case name_of_idf thy nsp_mem m
of SOME m =>
trns
- |> debug 5 (fn _ => "trying defgen class member for " ^ quote m)
+ |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
|> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
|-> (fn cls => succeed Undef)
| _ =>
trns |> fail ("no class member found for " ^ quote m)
fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
- case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
+ case co_of_idf thy tabs co
of SOME (co, dtco) =>
trns
- |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
+ |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
|> ensure_def_tyco thy tabs dtco
|-> (fn dtco => succeed Undef)
| _ =>
@@ -827,7 +722,7 @@
val idf = idf_of_const thy tabs (c, ty);
in
trns
- |> debug 4 (fn _ => "generating constant " ^ quote c)
+ |> debug_msg (fn _ => "generating constant " ^ quote c)
|> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
|> pair idf
end
@@ -865,7 +760,7 @@
|-> (fn (e, es) => pair (e `$$ es))
end
and exprsgen_term thy tabs =
- fold_map (exprgen_term thy tabs) o snd o devarify_term_typs
+ fold_map (exprgen_term thy tabs)
and exprsgen_eqs thy tabs =
apfst (map (fn (rhs::args) => (args, rhs)))
oo fold_burrow (exprsgen_term thy tabs)
@@ -889,37 +784,23 @@
val tys = Library.take (d, ((fst o strip_type) ty));
in
trns
- |> debug 10 (fn _ => "eta-expanding")
|> fold_map (exprgen_type thy tabs) tys
||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
|-> (fn (tys, e) => pair (vs ~~ tys `|--> e))
end
else if length ts > imax then
trns
- |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", "
- ^ string_of_int (length ts) ^ ")")
|> ag thy tabs ((f, ty), Library.take (imax, ts))
||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
|-> (fn (e, es) => pair (e `$$ es))
else
trns
- |> debug 10 (fn _ => "keeping arguments")
|> ag thy tabs ((f, ty), ts)
| NONE =>
trns
|> appgen_default thy tabs ((f, ty), ts);
-(* function extractors *)
-
-fun eqextr_defs thy (deftab, _) (c, ty) =
- Option.mapPartial (get_first (fn (ty', (thm, _)) =>
- if Sign.typ_instance thy (ty, ty')
- then SOME ([thm], ty')
- else NONE
- )) (Symtab.lookup deftab c);
-
-
(* parametrized generators, for instantiation in HOL *)
fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns =
@@ -987,9 +868,9 @@
of Type ("fun", [Type (dtco, _), _]) =>
(case f thy dtco
of [] => NONE
- | [eq] => SOME ((Codegen.preprocess thy [eq], NONE), ty)
- | eqs => SOME ((Codegen.preprocess thy eqs, SOME fals), ty))
- | _ => NONE)
+ | [eq] => SOME ((the o CodegenTheorems.preprocess_fun thy) [eq], NONE)
+ | eqs => SOME ((the o CodegenTheorems.preprocess_fun thy) eqs, SOME fals))
+ | _ => NONE) |> Option.map (fn ((ty, eqs), default) => ((eqs, default), ty))
| eqextr_eq f fals thy tabs _ =
NONE;
@@ -1041,32 +922,6 @@
fun mk_tabs thy =
let
- fun extract_defs thy =
- let
- fun dest thm =
- let
- val (lhs, rhs) = Logic.dest_equals (prop_of thm);
- val (t, args) = strip_comb lhs;
- val (c, ty) = dest_Const t
- in if forall is_Var args then SOME ((c, ty), thm) else NONE
- end handle TERM _ => NONE;
- fun prep_def def = (case Codegen.preprocess thy [def] of
- [def'] => def' | _ => error "mk_tabs: bad preprocessor");
- fun add_def thyname (name, _) =
- case (dest o prep_def o Thm.get_axiom thy) name
- of SOME ((c, ty), thm) =>
- Symtab.default (c, [])
- #> Symtab.map_entry c (cons (ty, (thm, thyname)))
- | NONE => I
- fun get_defs thy =
- let
- val thyname = Context.theory_name thy;
- val defs = (snd o #axioms o Theory.rep_theory) thy;
- in Symtab.fold (add_def thyname) defs end;
- in
- Symtab.empty
- |> fold get_defs (thy :: Theory.ancestors_of thy)
- end;
fun mk_insttab thy =
InstNameMangler.empty
|> Symtab.fold_map
@@ -1096,11 +951,20 @@
let
val c = "op =";
val ty = Sign.the_const_type thy c;
- fun inst dtco =
- map_atyps (fn _ => Type (dtco,
- (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
- val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
- val tys = map inst dtcos;
+ fun inst tyco =
+ let
+ val ty_inst =
+ tyco
+ |> Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy)
+ |> (fn SOME (Type.LogicalType i, _) => i)
+ |> Term.invent_names [] "'a"
+ |> map (fn v => (TVar ((v, 0), Sign.defaultS thy)))
+ |> (fn tys => Type (tyco, tys))
+ in map_atyps (fn _ => ty_inst) ty end;
+ val tys =
+ (Type.logical_types o Sign.tsig_of) thy
+ |> filter (fn tyco => (is_some oo try) (Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco) (Sign.defaultS thy))
+ |> map inst
in
(overltab1
|> Symtab.update_new (c, tys),
@@ -1117,11 +981,10 @@
in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
) (get_all_datatype_cons thy) [])
|-> (fn _ => I);
- val deftab = extract_defs thy;
val insttab = mk_insttab thy;
val overltabs = mk_overltabs thy;
val dtcontab = mk_dtcontab thy;
- in (deftab, (insttab, overltabs, dtcontab)) end;
+ in (Symtab.empty, (insttab, overltabs, dtcontab)) end;
fun get_serializer target =
case Symtab.lookup (!serializers) target
@@ -1132,6 +995,20 @@
map_codegen_data (fn (modl, gens, target_data, logic_data) =>
(f modl, gens, target_data, logic_data));
+(*fun delete_defs NONE thy =
+ map_module (K CodegenThingol.empty_module) thy
+ | delete_defs (SOME c) thy =
+ let
+ val tabs = mk_tabs thy;
+ in
+ map_module (CodegenThingol.purge_module []) thy
+ end;
+does not make sense:
+* primitve definitions have to be kept
+* *all* overloaded defintitions for a constant have to be purged
+* precondition: improved representation of definitions hidden by customary serializations
+*)
+
fun expand_module init gen arg thy =
(#modl o CodegenData.get) thy
|> start_transact init (gen thy (mk_tabs thy) arg)
@@ -1176,7 +1053,7 @@
fun codegen_term t thy =
thy
- |> expand_module NONE exprsgen_term [Codegen.preprocess_term thy t]
+ |> expand_module NONE exprsgen_term [CodegenTheorems.preprocess_term thy t]
|-> (fn [t] => pair t);
val is_dtcon = has_nsp nsp_dtcon;
@@ -1208,8 +1085,13 @@
fun read_typ thy =
Sign.read_typ (thy, K NONE);
-fun read_const thy =
- (dest_Const o Sign.read_term thy);
+fun read_const thy raw_t =
+ let
+ val t = Sign.read_term thy raw_t
+ in case try dest_Const t
+ of SOME c => c
+ | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
+ end;
fun read_quote get reader gen raw thy =
thy
@@ -1389,6 +1271,11 @@
|-> (fn cs => serialize cs)
end;
+fun purge_consts raw_ts thy =
+ let
+ val cs = map (read_const thy) raw_ts;
+ in fold CodegenTheorems.purge_defs cs thy end;
+
structure P = OuterParse
and K = OuterKeyword
@@ -1396,10 +1283,12 @@
val (generateK, serializeK,
primclassK, primtycoK, primconstK,
- syntax_classK, syntax_tycoK, syntax_constK, aliasK) =
+ syntax_classK, syntax_tycoK, syntax_constK,
+ purgeK, aliasK) =
("code_generate", "code_serialize",
"code_primclass", "code_primtyco", "code_primconst",
- "code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias");
+ "code_syntax_class", "code_syntax_tyco", "code_syntax_const",
+ "code_purge", "code_alias");
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
@@ -1421,14 +1310,8 @@
))
);
-val aliasP =
- OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
- Scan.repeat1 (P.name -- P.name)
- >> (Toplevel.theory oo fold) add_alias
- );
-
val primclassP =
- OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl (
+ OuterSyntax.command primclassK "define target-language specific class" K.thy_decl (
P.xname
-- Scan.repeat1 (P.name -- P.text)
>> (fn (raw_class, primdefs) =>
@@ -1436,7 +1319,7 @@
);
val primtycoP =
- OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl (
+ OuterSyntax.command primtycoK "define target-language specific type constructor" K.thy_decl (
P.xname
-- Scan.repeat1 (P.name -- P.text)
>> (fn (raw_tyco, primdefs) =>
@@ -1444,7 +1327,7 @@
);
val primconstP =
- OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
+ OuterSyntax.command primconstK "define target-language specific constant" K.thy_decl (
P.term
-- Scan.repeat1 (P.name -- P.text)
>> (fn (raw_const, primdefs) =>
@@ -1487,16 +1370,21 @@
(fn (target, modifier) => modifier target)
);
-val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP,
- primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP];
-
-
+val purgeP =
+ OuterSyntax.command purgeK "purge all defintions for constant" K.thy_decl (
+ Scan.repeat1 P.term
+ >> (Toplevel.theory o purge_consts)
+ );
-(** theory setup **)
+val aliasP =
+ OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
+ Scan.repeat1 (P.name -- P.name)
+ >> (Toplevel.theory oo fold) add_alias
+ );
-val _ = Context.add_setup (
- add_eqextr ("defs", eqextr_defs)
-);
+val _ = OuterSyntax.add_parsers [generateP, serializeP,
+ primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP,
+ purgeP, aliasP];
end; (* local *)
--- a/src/Pure/Tools/codegen_serializer.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Thu Apr 06 16:08:25 2006 +0200
@@ -39,7 +39,7 @@
struct
open BasicCodegenThingol;
-val debug = CodegenThingol.debug;
+val debug_msg = CodegenThingol.debug_msg;
(** generic serialization **)
@@ -244,15 +244,16 @@
of [] => NONE
| ps => (SOME o Pretty.block) ps)
end;
- fun from_module' imps ((name_qual, name), defs) =
- from_module imps ((name_qual, name), defs) |> postprocess name_qual;
+ fun from_module' resolv imps ((name_qual, name), defs) =
+ from_module resolv imps ((name_qual, name), defs)
+ |> postprocess (resolv name_qual);
in
module
- |> debug 3 (fn _ => "selecting submodule...")
- |> (if is_some select then (CodegenThingol.partof o the) select else I)
- |> debug 3 (fn _ => "preprocessing...")
+ |> debug_msg (fn _ => "selecting submodule...")
+ |> (if is_some select then (CodegenThingol.project_module o the) select else I)
+ |> debug_msg (fn _ => "preprocessing...")
|> preprocess
- |> debug 3 (fn _ => "serializing...")
+ |> debug_msg (fn _ => "serializing...")
|> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
from_module' validator postproc nspgrp name_root
|> K ()
@@ -416,7 +417,10 @@
fun ml_from_sortlookup fxy lss =
let
fun from_label l =
- Pretty.block [str "#", ml_from_label l];
+ Pretty.block [str "#",
+ if (is_some o Int.fromString) l then str l
+ else ml_from_label l
+ ];
fun from_lookup fxy [] p = p
| from_lookup fxy [l] p =
brackify fxy [
@@ -552,10 +556,11 @@
ml_from_expr NOBR be
]
in brackify fxy (
- str "case"
+ str "(case"
:: typify dty (ml_from_expr NOBR de)
:: mk_clause "of" bse
:: map (mk_clause "|") bses
+ @ [str ")"]
) end
| ml_from_expr _ e =
error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
@@ -806,7 +811,7 @@
fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
let
- fun ml_from_module _ ((_, name), ps) =
+ fun ml_from_module resolv _ ((_, name), ps) =
Pretty.chunks ([
str ("structure " ^ name ^ " = "),
str "struct",
@@ -832,12 +837,12 @@
else 0;
fun preprocess const_syntax module =
module
- |> debug 3 (fn _ => "eta-expanding...")
+ |> debug_msg (fn _ => "eta-expanding...")
|> CodegenThingol.eta_expand (eta_expander module const_syntax)
- |> debug 3 (fn _ => "eta-expanding polydefs...")
+ |> debug_msg (fn _ => "eta-expanding polydefs...")
|> CodegenThingol.eta_expand_poly
- |> debug 3 (fn _ => "unclashing expression/type variables...")
- |> CodegenThingol.unclash_vars_tvars;
+ (*|> debug 3 (fn _ => "unclashing expression/type variables...")
+ |> CodegenThingol.unclash_vars_tvars*);
val parse_multi =
OuterParse.name
#-> (fn "dir" =>
@@ -871,12 +876,8 @@
fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
resolver prefix defs =
let
- fun resolv s = if NameSpace.is_qualified s
- then resolver "" s
- else if nth_string s 0 = "~"
- then enclose "(" ")" ("negate " ^ unprefix "~" s)
- else s;
- val resolv_here = (resolver o NameSpace.base) prefix;
+ val resolv = resolver "";
+ val resolv_here = resolver prefix;
fun hs_from_sctxt vs =
let
fun from_class cls =
@@ -895,11 +896,11 @@
|> from_sctxt
end;
fun hs_from_tycoexpr fxy (tyco, tys) =
- brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
+ brackify fxy (str tyco :: map (hs_from_type BR) tys)
and hs_from_type fxy (tycoexpr as tyco `%% tys) =
(case tyco_syntax tyco
of NONE =>
- hs_from_tycoexpr fxy (tyco, tys)
+ hs_from_tycoexpr fxy (resolv tyco, tys)
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
then error ("number of argument mismatch in customary serialization: "
@@ -944,7 +945,8 @@
end
| hs_from_expr fxy (INum ((n, ty), _)) =
brackify BR [
- (str o IntInf.toString) n,
+ (str o (fn s => if nth_string s 0 = "~"
+ then enclose "(" ")" ("negate " ^ unprefix "~" s) else s) o IntInf.toString) n,
str "::",
hs_from_type NOBR ty
]
@@ -1099,7 +1101,7 @@
] @ [
"Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate"
];
- fun hs_from_module imps ((_, name), ps) =
+ fun hs_from_module resolv imps ((_, name), ps) =
(Pretty.chunks) (
str ("module " ^ name ^ " where")
:: map (str o prefix "import qualified ") imps @ (
@@ -1121,7 +1123,7 @@
|> the_default 0;
fun preprocess const_syntax module =
module
- |> debug 3 (fn _ => "eta-expanding...")
+ |> debug_msg (fn _ => "eta-expanding...")
|> CodegenThingol.eta_expand (eta_expander const_syntax)
in
(Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
--- a/src/Pure/Tools/codegen_theorems.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Thu Apr 06 16:08:25 2006 +0200
@@ -1,4 +1,4 @@
-(* Title: Pure/Tools/CODEGEN_THEOREMS.ML
+(* Title: Pure/Tools/codegen_theorems.ML
ID: $Id$
Author: Florian Haftmann, TU Muenchen
@@ -9,11 +9,31 @@
sig
val add_notify: (string option -> theory -> theory) -> theory -> theory;
val add_preproc: (theory -> thm list -> thm list) -> theory -> theory;
- val add_funn: thm -> theory -> theory;
+ val add_fun_extr: (theory -> string * typ -> thm list) -> theory -> theory;
+ val add_datatype_extr: (theory -> string
+ -> (((string * sort) list * (string * typ list) list) * tactic) option)
+ -> theory -> theory;
+ val add_fun: thm -> theory -> theory;
val add_pred: thm -> theory -> theory;
val add_unfold: thm -> theory -> theory;
- val preprocess: theory -> thm list -> thm list;
+ val del_def: thm -> theory -> theory;
+ val del_unfold: thm -> theory -> theory;
+ val purge_defs: string * typ -> theory -> theory;
+
+ val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
+ val preprocess: theory -> (thm -> typ) option -> thm list -> thm list;
+ val preprocess_fun: theory -> thm list -> (typ * thm list) option;
val preprocess_term: theory -> term -> term;
+ val get_funs: theory -> string * typ -> (typ * thm list) option;
+ val get_datatypes: theory -> string
+ -> (((string * sort) list * (string * typ list) list) * thm list) option;
+
+ val debug: bool ref;
+ val debug_msg: ('a -> string) -> 'a -> 'a;
+
+ val print_thms: theory -> unit;
+ val init_obj: theory -> string -> string * (thm list -> tactic) -> string * (thm list -> tactic)
+ -> string * (thm list -> tactic) -> string * (thm list -> tactic) -> unit;
end;
structure CodegenTheorems: CODEGEN_THEOREMS =
@@ -21,16 +41,126 @@
(** auxiliary **)
-fun dest_funn thm =
- case try (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals o prop_of) thm
- of SOME c => SOME (c, thm)
+val debug = ref false;
+fun debug_msg f x = (if !debug then Output.debug (f x) else (); x);
+
+
+(** object logic **)
+
+val obj_bool_ref : string option ref = ref NONE;
+val obj_true_ref : string option ref = ref NONE;
+val obj_false_ref : string option ref = ref NONE;
+val obj_and_ref : string option ref = ref NONE;
+val obj_eq_ref : string option ref = ref NONE;
+val obj_eq_elim_ref : thm option ref = ref NONE;
+fun idem c = (the o !) c;
+
+fun mk_tf sel =
+ let
+ val bool_typ = Type (idem obj_bool_ref, []);
+ val name = idem
+ (if sel then obj_true_ref else obj_false_ref);
+ in
+ Const (name, bool_typ)
+ end handle Option => error "no object logic setup for code theorems";
+
+fun mk_obj_conj (x, y) =
+ let
+ val bool_typ = Type (idem obj_bool_ref, []);
+ in
+ Const (idem obj_and_ref, bool_typ --> bool_typ --> bool_typ) $ x $ y
+ end handle Option => error "no object logic setup for code theorems";
+
+fun mk_obj_eq (x, y) =
+ let
+ val bool_typ = Type (idem obj_bool_ref, []);
+ in
+ Const (idem obj_eq_ref, type_of x --> type_of y --> bool_typ) $ x $ y
+ end handle Option => error "no object logic setup for code theorems";
+
+fun is_obj_eq c =
+ c = idem obj_eq_ref
+ handle Option => error "no object logic setup for code theorems";
+
+fun mk_bool_eq ((x, y), rhs) =
+ let
+ val bool_typ = Type (idem obj_bool_ref, []);
+ in
+ Logic.mk_equals (
+ (mk_obj_eq (x, y)),
+ rhs
+ )
+ end handle Option => error "no object logic setup for code theorems";
+
+fun elim_obj_eq thm = rewrite_rule [idem obj_eq_elim_ref] thm
+ handle Option => error "no object logic setup for code theorems";
+
+fun init_obj thy bohl (truh, truh_tac) (fals, fals_tac) (ant, ant_tac) (eq, eq_tac) =
+ let
+ val _ = if (is_some o !) obj_bool_ref
+ then error "already set" else ()
+ val bool_typ = Type (bohl, []);
+ val free_typ = TFree ("'a", Sign.defaultS thy);
+ val var_x = Free ("x", free_typ);
+ val var_y = Free ("y", free_typ);
+ val prop_P = Free ("P", bool_typ);
+ val prop_Q = Free ("Q", bool_typ);
+ val _ = Goal.prove thy [] []
+ (ObjectLogic.ensure_propT thy (Const (truh, bool_typ))) truh_tac;
+ val _ = Goal.prove thy ["P"] [ObjectLogic.ensure_propT thy (Const (fals, bool_typ))]
+ (ObjectLogic.ensure_propT thy prop_P) fals_tac;
+ val _ = Goal.prove thy ["P", "Q"] [ObjectLogic.ensure_propT thy prop_P, ObjectLogic.ensure_propT thy prop_Q]
+ (ObjectLogic.ensure_propT thy (Const (ant, bool_typ --> bool_typ --> bool_typ) $ prop_P $ prop_Q)) ant_tac;
+ val atomize_eq = Goal.prove thy ["x", "y"] []
+ (Logic.mk_equals (
+ Logic.mk_equals (var_x, var_y),
+ ObjectLogic.ensure_propT thy
+ (Const (eq, free_typ --> free_typ --> bool_typ) $ var_x $ var_y))) eq_tac;
+ in
+ obj_bool_ref := SOME bohl;
+ obj_true_ref := SOME truh;
+ obj_false_ref := SOME fals;
+ obj_and_ref := SOME ant;
+ obj_eq_ref := SOME eq;
+ obj_eq_elim_ref := SOME (Thm.symmetric atomize_eq)
+ end;
+
+
+(** auxiliary **)
+
+fun destr_fun thy thm =
+ case try (
+ prop_of
+ #> ObjectLogic.drop_judgment thy
+ #> Logic.dest_equals
+ #> fst
+ #> strip_comb
+ #> fst
+ #> dest_Const
+ ) (elim_obj_eq thm)
+ of SOME c_ty => SOME (c_ty, thm)
| NONE => NONE;
+fun dest_fun thy thm =
+ case destr_fun thy thm
+ of SOME x => x
+ | NONE => error ("not a function equation: " ^ string_of_thm thm);
+
fun dest_pred thm =
case try (fst o dest_Const o fst o strip_comb o snd o Logic.dest_implies o prop_of) thm
of SOME c => SOME (c, thm)
| NONE => NONE;
+fun getf_first [] _ = NONE
+ | getf_first (f::fs) x = case f x
+ of NONE => getf_first fs x
+ | y as SOME x => y;
+
+fun getf_first_list [] x = []
+ | getf_first_list (f::fs) x = case f x
+ of [] => getf_first_list fs x
+ | xs => xs;
+
(** theory data **)
@@ -46,49 +176,113 @@
mk_procs (AList.merge (op =) (K true) (preprocs1, preprocs2),
AList.merge (op =) (K true) (notify1, notify2));
+datatype extrs = Extrs of {
+ funs: (serial * (theory -> string * typ -> thm list)) list,
+ datatypes: (serial * (theory -> string -> (((string * sort) list * (string * typ list) list) * tactic) option)) list
+};
+
+fun mk_extrs (funs, datatypes) = Extrs { funs = funs, datatypes = datatypes };
+fun map_extrs f (Extrs { funs, datatypes }) = mk_extrs (f (funs, datatypes));
+fun merge_extrs _ (Extrs { funs = funs1, datatypes = datatypes1 },
+ Extrs { funs = funs2, datatypes = datatypes2 }) =
+ mk_extrs (AList.merge (op =) (K true) (funs1, funs2),
+ AList.merge (op =) (K true) (datatypes1, datatypes2));
+
datatype codethms = Codethms of {
- funns: thm list Symtab.table,
+ funs: thm list Symtab.table,
preds: thm list Symtab.table,
unfolds: thm list
};
-fun mk_codethms ((funns, preds), unfolds) =
- Codethms { funns = funns, preds = preds, unfolds = unfolds };
-fun map_codethms f (Codethms { funns, preds, unfolds }) =
- mk_codethms (f ((funns, preds), unfolds));
-fun merge_codethms _ (Codethms { funns = funns1, preds = preds1, unfolds = unfolds1 },
- Codethms { funns = funns2, preds = preds2, unfolds = unfolds2 }) =
- mk_codethms ((Symtab.join (K (uncurry (fold (insert eq_thm)))) (funns1, funns2),
+fun mk_codethms ((funs, preds), unfolds) =
+ Codethms { funs = funs, preds = preds, unfolds = unfolds };
+fun map_codethms f (Codethms { funs, preds, unfolds }) =
+ mk_codethms (f ((funs, preds), unfolds));
+fun merge_codethms _ (Codethms { funs = funs1, preds = preds1, unfolds = unfolds1 },
+ Codethms { funs = funs2, preds = preds2, unfolds = unfolds2 }) =
+ mk_codethms ((Symtab.join (K (uncurry (fold (insert eq_thm)))) (funs1, funs2),
Symtab.join (K (uncurry (fold (insert eq_thm)))) (preds1, preds2)),
fold (insert eq_thm) unfolds1 unfolds2);
+datatype codecache = Codecache of {
+ funs: thm list Symtab.table,
+ datatypes: (string * typ list) list Symtab.table
+};
+
+fun mk_codecache (funs, datatypes) = Codecache { funs = funs, datatypes = datatypes };
+fun map_codecache f (Extrs { funs, datatypes }) = Codecache (f (funs, datatypes));
+fun merge_codecache _ (Codecache { funs = funs1, datatypes = datatypes1 },
+ Extrs { funs = funs2, datatypes = datatypes2 }) =
+ mk_codecache (Symtab.empty, Symtab.empty);
+
datatype T = T of {
procs: procs,
+ extrs: extrs,
codethms: codethms
};
-fun mk_T (procs, codethms) = T { procs = procs, codethms = codethms };
-fun map_T f (T { procs, codethms }) = mk_T (f (procs, codethms));
-fun merge_T pp (T { procs = procs1, codethms = codethms1 },
- T { procs = procs2, codethms = codethms2 }) =
- mk_T (merge_procs pp (procs1, procs2), merge_codethms pp (codethms1, codethms2));
+fun mk_T (procs, (extrs, codethms)) = T { procs = procs, extrs = extrs, codethms = codethms };
+fun map_T f (T { procs, extrs, codethms }) = mk_T (f (procs, (extrs, codethms)));
+fun merge_T pp (T { procs = procs1, extrs = extrs1, codethms = codethms1 },
+ T { procs = procs2, extrs = extrs2, codethms = codethms2 }) =
+ mk_T (merge_procs pp (procs1, procs2), (merge_extrs pp (extrs1, extrs2), merge_codethms pp (codethms1, codethms2)));
structure CodegenTheorems = TheoryDataFun
(struct
val name = "Pure/CodegenTheorems";
type T = T;
val empty = mk_T (mk_procs ([], []),
- mk_codethms ((Symtab.empty, Symtab.empty), []));
+ (mk_extrs ([], []), mk_codethms ((Symtab.empty, Symtab.empty), [])));
val copy = I;
val extend = I;
val merge = merge_T;
- fun print _ _ = ();
+ fun print (thy : theory) (data : T) =
+ let
+ val codethms = (fn T { codethms, ... } => codethms) data;
+ val funs = (Symtab.dest o (fn Codethms { funs, ... } => funs)) codethms;
+ val preds = (Symtab.dest o (fn Codethms { preds, ... } => preds)) codethms;
+ val unfolds = (fn Codethms { unfolds, ... } => unfolds) codethms;
+ in
+ (Pretty.writeln o Pretty.block o Pretty.fbreaks) ([
+ Pretty.str "code generation theorems:",
+ Pretty.str "function theorems:" ] @
+ Pretty.fbreaks (
+ map (fn (c, thms) =>
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str c :: map Display.pretty_thm thms
+ )
+ ) funs
+ ) @ [
+ Pretty.str "predicate theorems:" ] @
+ Pretty.fbreaks (
+ map (fn (c, thms) =>
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str c :: map Display.pretty_thm thms
+ )
+ ) preds
+ ) @ [
+ Pretty.str "unfolding theorems:",
+ (Pretty.block o Pretty.fbreaks o map Display.pretty_thm) unfolds
+ ])
+ end;
end);
val _ = Context.add_setup CodegenTheorems.init;
-
+val print_thms = CodegenTheorems.print;
-(** notifiers and preprocessors **)
+local
+ val the_procs = (fn T { procs = Procs procs, ... } => procs) o CodegenTheorems.get
+ val the_extrs = (fn T { extrs = Extrs extrs, ... } => extrs) o CodegenTheorems.get
+ val the_codethms = (fn T { codethms = Codethms codethms, ... } => codethms) o CodegenTheorems.get
+in
+ val the_preprocs = (fn { preprocs, ... } => map snd preprocs) o the_procs;
+ val the_notify = (fn { notify, ... } => map snd notify) o the_procs;
+ val the_funs_extrs = (fn { funs, ... } => map snd funs) o the_extrs;
+ val the_datatypes_extrs = (fn { datatypes, ... } => map snd datatypes) o the_extrs;
+ val the_funs = (fn { funs, ... } => funs) o the_codethms;
+ val the_preds = (fn { preds, ... } => preds) o the_codethms;
+ val the_unfolds = (fn { unfolds, ... } => unfolds) o the_codethms;
+end (*local*);
fun add_notify f =
CodegenTheorems.map (map_T (fn (procs, codethms) =>
@@ -96,8 +290,7 @@
(preprocs, (serial (), f) :: notify)), codethms)));
fun notify_all c thy =
- fold (fn f => f c) (((fn Procs { notify, ... } => map snd notify)
- o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy) thy;
+ fold (fn f => f c) (the_notify thy) thy;
fun add_preproc f =
CodegenTheorems.map (map_T (fn (procs, codethms) =>
@@ -105,44 +298,220 @@
((serial (), f) :: preprocs, notify)), codethms)))
#> notify_all NONE;
-fun preprocess thy =
- fold (fn f => f thy) (((fn Procs { preprocs, ... } => map snd preprocs)
- o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy);
+fun add_fun_extr f =
+ CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs |> map_extrs (fn (funs, datatypes) =>
+ ((serial (), f) :: funs, datatypes)), codethms))))
+ #> notify_all NONE;
+
+fun add_datatype_extr f =
+ CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs |> map_extrs (fn (funs, datatypes) =>
+ (funs, (serial (), f) :: datatypes)), codethms))))
+ #> notify_all NONE;
+
+fun add_fun thm thy =
+ case destr_fun thy thm
+ of SOME ((c, _), _) =>
+ thy
+ |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) =>
+ ((funs |> Symtab.default (c, []) |> Symtab.map_entry c (fn thms => thms @ [thm]), preds), unfolds))))))
+ |> notify_all (SOME c)
+ | NONE => tap (fn _ => warning ("not a function equation: " ^ string_of_thm thm)) thy;
+
+fun add_pred thm thy =
+ case dest_pred thm
+ of SOME (c, _) =>
+ thy
+ |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) =>
+ ((funs, preds |> Symtab.default (c, []) |> Symtab.map_entry c (fn thms => thms @ [thm])), unfolds))))))
+ |> notify_all (SOME c)
+ | NONE => tap (fn _ => warning ("not a predicate clause: " ^ string_of_thm thm)) thy;
+
+fun add_unfold thm =
+ CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn (defs, unfolds) =>
+ (defs, thm :: unfolds))))))
+ #> notify_all NONE;
+
+fun del_def thm thy =
+ case destr_fun thy thm
+ of SOME ((c, _), thm) =>
+ thy
+ |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) =>
+ ((funs |> Symtab.map_entry c (remove eq_thm thm), preds), unfolds))))))
+ |> notify_all (SOME c)
+ | NONE => case dest_pred thm
+ of SOME (c, thm) =>
+ thy
+ |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) =>
+ ((funs, preds |> Symtab.map_entry c (remove eq_thm thm)), unfolds))))))
+ |> notify_all (SOME c)
+ | NONE => error ("no code theorem to delete");
+
+fun del_unfold thm =
+ CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn (defs, unfolds) =>
+ (defs, remove eq_thm thm unfolds))))))
+ #> notify_all NONE;
+
+fun purge_defs (c, ty) thy =
+ thy
+ |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) =>
+ (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) =>
+ ((funs |> Symtab.map_entry c
+ (filter (fn thm => Sign.typ_instance thy ((snd o fst o dest_fun thy) thm, ty))),
+ preds |> Symtab.update (c, [])), unfolds))))))
+ |> notify_all (SOME c);
+
+
+(** preprocessing **)
+
+fun common_typ thy _ [] = []
+ | common_typ thy _ [thm] = [thm]
+ | common_typ thy extract_typ thms =
+ let
+ fun incr_thm thm max =
+ let
+ val thm' = incr_indexes max thm;
+ val max' = (maxidx_of_typ o type_of o prop_of) thm' + 1;
+ in (thm', max') end;
+ val (thms', maxidx) = fold_map incr_thm thms 0;
+ val (ty1::tys) = map extract_typ thms;
+ fun unify ty = Type.unify (Sign.tsig_of thy) (ty1, ty);
+ val (env, _) = fold unify tys (Vartab.empty, maxidx)
+ val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
+ cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
+ in map (Thm.instantiate (instT, [])) thms end;
+
+fun preprocess thy extract_typ thms =
+ thms
+ |> map (Thm.transfer thy)
+ |> fold (fn f => f thy) (the_preprocs thy)
+ |> map (rewrite_rule (the_unfolds thy))
+ |> (if is_some extract_typ then common_typ thy (the extract_typ) else I)
+ |> Drule.conj_intr_list
+ |> Drule.zero_var_indexes
+ |> Drule.conj_elim_list
+ |> map Drule.unvarifyT
+ |> map Drule.unvarify;
+
+fun preprocess_fun thy thms =
+ let
+ fun tap_typ [] = NONE
+ | tap_typ (thms as (thm::_)) = SOME ((snd o fst o dest_fun thy) thm, thms)
+ in
+ thms
+ |> map elim_obj_eq
+ |> preprocess thy (SOME (snd o fst o dest_fun thy))
+ |> tap_typ
+ end;
fun preprocess_term thy t =
let
- val x = Free (variant (add_term_names (t, [])) "x", fastype_of t);
- (* fake definition *)
+ val x = Free (variant (add_term_names (t, [])) "a", 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 (preprocess thy [eq]) of
+ in case map prop_of (preprocess thy NONE [eq]) of
[Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
| _ => err ()
end;
-fun add_unfold thm =
- CodegenTheorems.map (map_T (fn (procs, codethms) =>
- (procs, codethms |> map_codethms (fn (defs, unfolds) =>
- (defs, thm :: unfolds)))))
+
+(** retrieval **)
+
+fun get_funs thy (c, ty) =
+ let
+ val filter_typ = Library.mapfilter (fn ((_, ty'), thm) =>
+ if Sign.typ_instance thy (ty', ty)
+ orelse Sign.typ_instance thy (ty, ty')
+ then SOME thm else debug_msg (fn _ => "dropping " ^ string_of_thm thm) NONE);
+ val thms_funs =
+ (these o Symtab.lookup (the_funs thy)) c
+ |> map (dest_fun thy)
+ |> filter_typ;
+ val thms = case thms_funs
+ of [] =>
+ Defs.specifications_of (Theory.defs_of thy) c
+ |> map (PureThy.get_thms thy o Name o fst o snd)
+ |> Library.flat
+ |> append (getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty))
+ |> map (dest_fun thy)
+ |> filter_typ
+ | thms => thms
+ in
+ thms
+ |> preprocess_fun thy
+ end;
-fun add_funn thm =
- case dest_funn thm
- of SOME (c, thm) =>
- CodegenTheorems.map (map_T (fn (procs, codethms) =>
- (procs, codethms |> map_codethms (fn ((funns, preds), unfolds) =>
- ((funns |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm]), preds), unfolds)))))
- | NONE => error ("not a function equation: " ^ string_of_thm thm);
+fun get_datatypes thy dtco =
+ let
+ val truh = mk_tf true;
+ val fals = mk_tf false;
+ fun mk_lhs vs ((co1, tys1), (co2, tys2)) =
+ let
+ val dty = Type (dtco, map TFree vs);
+ val (xs1, xs2) = chop (length tys1) (Term.invent_names [] "x" (length tys1 + length tys2));
+ val frees1 = map2 (fn x => fn ty => Free (x, ty)) xs1 tys1;
+ val frees2 = map2 (fn x => fn ty => Free (x, ty)) xs2 tys2;
+ fun zip_co co xs tys = list_comb (Const (co,
+ tys ---> dty), map2 (fn x => fn ty => Free (x, ty)) xs tys);
+ in
+ ((frees1, frees2), (zip_co co1 xs1 tys1, zip_co co2 xs2 tys2))
+ end;
+ fun mk_rhs [] [] = truh
+ | mk_rhs xs ys = foldr1 mk_obj_conj (map2 (curry mk_obj_eq) xs ys);
+ fun mk_eq vs (args as ((co1, _), (co2, _))) (inj, dist) =
+ if co1 = co2
+ then let
+ val ((fs1, fs2), lhs) = mk_lhs vs args;
+ val rhs = mk_rhs fs1 fs2;
+ in (mk_bool_eq (lhs, rhs) :: inj, dist) end
+ else let
+ val (_, lhs) = mk_lhs vs args;
+ in (inj, mk_bool_eq (lhs, fals) :: dist) end;
+ fun mk_eqs (vs, cos) =
+ let val cos' = rev cos
+ in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end;
+ fun mk_eq_thms tac vs_cos =
+ map (fn t => (Goal.prove thy [] []
+ (ObjectLogic.ensure_propT thy t) (K tac))) (mk_eqs vs_cos);
+ in
+ case getf_first (map (fn f => f thy) (the_datatypes_extrs thy)) dtco
+ of NONE => NONE
+ | SOME (vs_cos, tac) => SOME (vs_cos, mk_eq_thms tac vs_cos)
+ end;
-fun add_pred thm =
- case dest_pred thm
- of SOME (c, thm) =>
- CodegenTheorems.map (map_T (fn (procs, codethms) =>
- (procs, codethms |> map_codethms (fn ((funns, preds), unfolds) =>
- ((funns, preds |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm])), unfolds)))))
- | NONE => error ("not a predicate clause: " ^ string_of_thm thm);
+fun get_eq thy (c, ty) =
+ if is_obj_eq c
+ then case get_datatypes thy ((fst o dest_Type o hd o fst o strip_type) ty)
+ of SOME (_, thms) => thms
+ | _ => []
+ else [];
-(** isar **)
+(** code attributes and setup **)
-end; (* struct *)
+local
+ fun add_simple_attribute (name, f) =
+ (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
+ (Context.map_theory o f);
+in
+ val _ = map (Context.add_setup o add_simple_attribute) [
+ ("fun", add_fun),
+ ("pred", add_pred),
+ ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
+ ("unfolt", add_unfold),
+ ("nofold", del_unfold)
+ ]
+end; (*local*)
+
+val _ = Context.add_setup (add_fun_extr get_eq);
+
+end; (*struct*)
--- a/src/Pure/Tools/codegen_thingol.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Thu Apr 06 16:08:25 2006 +0200
@@ -84,12 +84,13 @@
val pretty_module: module -> Pretty.T;
val pretty_deps: module -> Pretty.T;
val empty_module: module;
+ val get_def: module -> string -> def;
val add_prim: string -> (string * prim list) -> module -> module;
val ensure_prim: string -> string -> module -> module;
- val get_def: module -> string -> def;
val merge_module: module * module -> module;
val diff_module: module * module -> (string * def) list;
- val partof: string list -> module -> module;
+ val project_module: string list -> module -> module;
+ val purge_module: string list -> module -> module;
val has_nsp: string -> string -> bool;
val succeed: 'a -> transact -> 'a transact_fin;
val fail: string -> transact -> 'a transact_fin;
@@ -101,13 +102,13 @@
val eta_expand_poly: module -> module;
val unclash_vars_tvars: module -> module;
- val debug_level: int ref;
- val debug: int -> ('a -> string) -> 'a -> 'a;
+ val debug: bool ref;
+ val debug_msg: ('a -> string) -> 'a -> 'a;
val soft_exc: bool ref;
val serialize:
((string -> string -> string) -> string -> (string * def) list -> 'a option)
- -> (string list -> (string * string) * 'a list -> 'a option)
+ -> ((string -> string) -> string list -> (string * string) * 'a list -> 'a option)
-> (string -> string option)
-> (string * string -> string)
-> string list list -> string -> module -> 'a option;
@@ -118,8 +119,8 @@
(** auxiliary **)
-val debug_level = ref 0;
-fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x);
+val debug = ref false;
+fun debug_msg f x = (if !debug then Output.debug (f x) else (); x);
val soft_exc = ref true;
fun unfoldl dest x =
@@ -204,11 +205,11 @@
val op `|--> = Library.foldr (op `|->);
val pretty_sortcontext =
- Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
+ Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
[Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
fun pretty_itype (tyco `%% tys) =
- Pretty.block (Pretty.str tyco :: map pretty_itype tys)
+ Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
| pretty_itype (ty1 `-> ty2) =
Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
| pretty_itype (ITyVar v) =
@@ -437,7 +438,7 @@
Pretty.str "<UNDEF>"
| pretty_def (Prim prims) =
Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">")
- | pretty_def (Fun (eqs, (_, ty))) =
+ | pretty_def (Fun (eqs, (sortctxt, ty))) =
Pretty.enum " |" "" "" (
map (fn (ps, body) =>
Pretty.block [
@@ -446,18 +447,20 @@
Pretty.brk 1,
pretty_iexpr body,
Pretty.str "::",
+ pretty_sortcontext sortctxt,
+ Pretty.str "/",
pretty_itype ty
]) eqs
)
| pretty_def (Typesyn (vs, ty)) =
Pretty.block [
- Pretty.list "(" ")" (pretty_sortcontext vs),
+ pretty_sortcontext vs,
Pretty.str " |=> ",
pretty_itype ty
]
| pretty_def (Datatype (vs, cs)) =
Pretty.block [
- Pretty.list "(" ")" (pretty_sortcontext vs),
+ pretty_sortcontext vs,
Pretty.str " |=> ",
Pretty.enum " |" "" ""
(map (fn (c, tys) => (Pretty.block o Pretty.breaks)
@@ -715,7 +718,9 @@
((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1)
in diff_modl [] modl12 [] end;
-fun partof names modl =
+local
+
+fun project_trans f names modl =
let
datatype pathnode = PN of (string list * (string * pathnode) list);
fun mk_ipath ([], base) (PN (defs, modls)) =
@@ -727,7 +732,7 @@
|> (pair defs #> PN);
fun select (PN (defs, modls)) (Module module) =
module
- |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
+ |> f (Graph.all_succs module (defs @ map fst modls))
|> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
|> Module;
in
@@ -737,16 +742,34 @@
|> dest_modl
end;
+in
+
+val project_module = project_trans Graph.subgraph;
+val purge_module = project_trans Graph.del_nodes;
+
+end; (*local*)
+
fun imports_of modl name =
let
+ (*fun submodules prfx modl =
+ cons prfx
+ #> Graph.fold_nodes
+ (fn (m, Module modl) => submodules (prfx @ [m]) modl
+ | (_, Def _) => I) modl;
+ fun get_modl name =
+ fold (fn n => fn modl => (dest_modl oo Graph.get_node) modl n) name modl*)
fun imports prfx [] modl =
[]
| imports prfx (m::ms) modl =
map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m))
- @ map single (Graph.imm_succs modl m);
+ @ map single (Graph.imm_succs modl m)
in
modl
|> imports [] name
+ (*|> cons name
+ |> map (fn name => submodules name (get_modl name) [])
+ |> Library.flat
+ |> remove (op =) name*)
|> map NameSpace.pack
end;
@@ -808,11 +831,11 @@
else
error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
^ (Pretty.output o Pretty.block o Pretty.breaks) [
- Pretty.list "(" ")" (pretty_sortcontext sortctxt''),
+ pretty_sortcontext sortctxt'',
Pretty.str "|=>",
pretty_itype ty''
] ^ " vs. " ^ (Pretty.output o Pretty.block o Pretty.breaks) [
- Pretty.list "(" ")" (pretty_sortcontext sortctxt'),
+ pretty_sortcontext sortctxt',
Pretty.str "|=>",
pretty_itype ty'
]
@@ -888,7 +911,7 @@
| SOME dep => msg ^ ", with dependency " ^ quote dep;
fun add_dp NONE = I
| add_dp (SOME dep) =
- debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
+ debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
#> add_dep (dep, name);
fun prep_def def modl =
(check_prep_def modl def, modl);
@@ -896,26 +919,25 @@
modl
|> (if can (get_def modl) name
then
- debug 9 (fn _ => "asserting node " ^ quote name)
+ debug_msg (fn _ => "asserting node " ^ quote name)
#> add_dp dep
else
- debug 9 (fn _ => "allocating node " ^ quote name)
+ debug_msg (fn _ => "allocating node " ^ quote name)
#> add_def (name, Undef)
#> add_dp dep
- #> debug 9 (fn _ => "creating node " ^ quote name)
+ #> debug_msg (fn _ => "creating node " ^ quote name)
#> select_generator (fn gname => "trying code generator "
^ gname ^ " for definition of " ^ quote name) name defgens
- #> debug 9 (fn _ => "checking creation of node " ^ quote name)
+ #> debug_msg (fn _ => "checking creation of node " ^ quote name)
#> check_fail msg'
#-> (fn def => prep_def def)
#-> (fn def =>
- debug 10 (fn _ => "addition of " ^ name
- ^ " := " ^ (Pretty.output o pretty_def) def)
- #> debug 10 (fn _ => "adding")
+ debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
+ #> debug_msg (fn _ => "adding")
#> add_def_incr (name, def)
- #> debug 10 (fn _ => "postprocessing")
+ #> debug_msg (fn _ => "postprocessing")
#> postprocess_def (name, def)
- #> debug 10 (fn _ => "adding done")
+ #> debug_msg (fn _ => "adding done")
))
|> pair dep
end;
@@ -1080,9 +1102,7 @@
val (ps', tab'') = get_path_name ps tab'
in (p' :: ps', tab'') end;
fun deresolv tab prefix name =
- if (is_some o Int.fromString) name
- then name
- else let
+ let
val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
val (_, SOME tab') = get_path_name common tab;
val (name', _) = get_path_name rem tab';
@@ -1104,13 +1124,14 @@
List.mapPartial (seri prfx)
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
and seri prfx ([(name, Module modl)]) =
- seri_module (map (resolver []) (imports_of module (prfx @ [name])))
+ seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name])))
(mk_name prfx name, mk_contents (prfx @ [name]) modl)
| seri prfx ds =
seri_defs sresolver (NameSpace.pack prfx)
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
in
- seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))
+ seri_module (resolver []) (imports_of module [])
+ (*map (resolver []) (Graph.strong_conn module |> List.concat |> rev)*)
(("", name_root), (mk_contents [] module))
end;
--- a/src/Pure/Tools/nbe.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/nbe.ML Thu Apr 06 16:08:25 2006 +0200
@@ -41,7 +41,7 @@
fun norm_by_eval_i t thy =
let
val nbe_tab = NBE_Data.get thy;
- val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
+ val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab)
(CodegenPackage.get_root_module thy);
val (t', thy') = CodegenPackage.codegen_term t thy;
val modl_new = CodegenPackage.get_root_module thy';
--- a/src/Pure/Tools/nbe_codegen.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML Thu Apr 06 16:08:25 2006 +0200
@@ -150,9 +150,8 @@
| consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2
| consts_of (AbsN (_, t)) = consts_of t;
val consts = consts_of t [];
- val the_const = AList.lookup (op =)
- (consts ~~ CodegenPackage.consts_of_idfs thy consts)
- #> the_default ("", dummyT);
+ val the_const = the o AList.lookup (op =)
+ (consts ~~ CodegenPackage.consts_of_idfs thy consts);
fun to_term bounds (C s) = Const (the_const s)
| to_term bounds (V s) = Free (s, dummyT)
| to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds)
--- a/src/Pure/codegen.ML Thu Apr 06 16:08:22 2006 +0200
+++ b/src/Pure/codegen.ML Thu Apr 06 16:08:25 2006 +0200
@@ -83,6 +83,7 @@
val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
val mk_deftab: theory -> deftab
+ val add_unfold: thm -> theory -> theory
val get_node: codegr -> string -> node
val add_edge: string * string -> codegr -> codegr
@@ -346,7 +347,7 @@
| _ => err ()
end;
-val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory
+fun add_unfold eqn =
let
val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
fun prep thy = map (fn th =>
@@ -356,9 +357,8 @@
then rewrite_rule [eqn] (Thm.transfer thy th)
else th
end)
- in add_preprocessor prep end);
+ in add_preprocessor prep end;
-val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
(**** associate constants with target language code ****)