--- a/src/Pure/Tools/ROOT.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML Tue Aug 08 08:19:30 2006 +0200
@@ -12,6 +12,7 @@
use "../codegen.ML";
(*code generator, 2nd generation*)
+use "codegen_names.ML";
use "codegen_theorems.ML";
use "codegen_thingol.ML";
use "codegen_serializer.ML";
--- a/src/Pure/Tools/class_package.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Tue Aug 08 08:19:30 2006 +0200
@@ -61,15 +61,18 @@
fun instantiations_of thy (ty, ty') =
let
+(* val _ = writeln "A"; *)
val vartab = typ_tvars ty;
+(* val _ = writeln "B"; *)
fun prep_vartab (v, (_, ty)) =
case (the o AList.lookup (op =) vartab) v
of [] => NONE
| sort => SOME ((v, sort), ty);
+(* val _ = writeln "C"; *)
in case try (Sign.typ_match thy (ty, ty')) Vartab.empty
- of NONE => NONE
+ of NONE => ((*writeln "D";*)NONE)
| SOME vartab =>
- SOME ((map_filter prep_vartab o Vartab.dest) vartab)
+ ((*writeln "E";*)SOME ((map_filter prep_vartab o Vartab.dest) vartab))
end;
@@ -640,16 +643,25 @@
fun sortlookups_const thy (c, typ_ctxt) =
let
+(* val _ = writeln c *)
val typ_decl = case AxClass.class_of_param thy c
of NONE => Sign.the_const_type thy c
| SOME class => case the_consts_sign thy class of (v, cs) =>
(Logic.legacy_varifyT o subst_clsvar v (TFree (v, [class])))
((the o AList.lookup (op =) cs) c)
+(* val _ = writeln "DECL" *)
+(* val _ = (writeln o Display.raw_string_of_typ) typ_decl; *)
+(* val _ = writeln "CTXT" *)
+(* val _ = (writeln o Display.raw_string_of_typ) typ_ctxt; *)
+(* val _ = writeln "(0)" *)
in
instantiations_of thy (typ_decl, typ_ctxt)
|> the
+(* |> tap (fn _ => writeln "(1)") *)
|> map (fn ((_, sort), ty) => sortlookup thy (sort, ty))
+(* |> tap (fn _ => writeln "(2)") *)
|> filter_out null
+(* |> tap (fn _ => writeln "(3)") *)
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/codegen_names.ML Tue Aug 08 08:19:30 2006 +0200
@@ -0,0 +1,387 @@
+(* Title: Pure/Tools/codegen_names.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Name policies for code generation: dissolving ad-hoc overloaded
+constants, prefixing any name by corresponding theory name,
+conversion to alphanumeric representation.
+Mappings are incrementally cached.
+*)
+
+signature CODEGEN_NAMES =
+sig
+ type tyco = string;
+ type const = string;
+ val class: theory -> class -> class
+ val class_rev: theory -> class -> class
+ val tyco: theory -> tyco -> tyco
+ val tyco_rev: theory -> tyco -> tyco
+ val instance: theory -> class * tyco -> string
+ val instance_rev: theory -> string -> class * tyco
+ val const: theory -> string * typ -> const
+ val const_rev: theory -> const -> string * typ
+ val force: (string * typ) * const -> theory -> theory
+ val read_const_typ: theory -> string -> string * typ
+ val read_const: theory -> string -> const
+ val purify_var: string -> string
+end;
+
+structure CodegenNames: CODEGEN_NAMES =
+struct
+
+
+(* theory data *)
+
+type tyco = string;
+type const = string;
+val inst_ord = prod_ord fast_string_ord fast_string_ord;
+val eq_inst = is_equal o inst_ord;
+val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
+val eq_const = is_equal o const_ord;
+
+structure Insttab =
+ TableFun(
+ type key = class * tyco;
+ val ord = inst_ord;
+ );
+
+structure Consttab =
+ TableFun(
+ type key = string * typ list;
+ val ord = const_ord;
+ );
+
+datatype names = Names of {
+ class: class Symtab.table * class Symtab.table,
+ tyco: tyco Symtab.table * tyco Symtab.table,
+ instance: string Insttab.table * (class * tyco) Symtab.table,
+ const: const Consttab.table * (string * typ list) Symtab.table
+}
+
+val empty_names = Names {
+ class = (Symtab.empty, Symtab.empty),
+ tyco = (Symtab.empty, Symtab.empty),
+ instance = (Insttab.empty, Symtab.empty),
+ const = (Consttab.empty, Symtab.empty)
+};
+
+local
+ fun mk_names (class, tyco, instance, const) =
+ Names { class = class, tyco = tyco, instance = instance, const = const};
+ fun map_names f (Names { class, tyco, instance, const }) =
+ mk_names (f (class, tyco, instance, const));
+ val eq_string = op = : string * string -> bool;
+in
+ fun merge_names (Names { class = (class1, classrev1), tyco = (tyco1, tycorev1),
+ instance = (instance1, instancerev1), const = (const1, constrev1) },
+ Names { class = (class2, classrev2), tyco = (tyco2, tycorev2),
+ instance = (instance2, instancerev2), const = (const2, constrev2) }) =
+ mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
+ (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
+ (Insttab.merge eq_string (instance1, instance2), Symtab.merge eq_inst (instancerev1, instancerev2)),
+ (Consttab.merge eq_string (const1, const2), Symtab.merge eq_const (constrev1, constrev2)));
+ fun map_class f = map_names
+ (fn (class, tyco, inst, const) => (f class, tyco, inst, const));
+ fun map_tyco f = map_names
+ (fn (class, tyco, inst, const) => (class, f tyco, inst, const));
+ fun map_inst f = map_names
+ (fn (class, tyco, inst, const) => (class, tyco, f inst, const));
+ fun map_const f = map_names
+ (fn (class, tyco, inst, const) => (class, tyco, inst, f const));
+
+end; (*local*)
+
+structure CodegenNamesData = TheoryDataFun
+(struct
+ val name = "Pure/codegen_names";
+ type T = names ref;
+ val empty = ref empty_names;
+ fun copy (ref names) = ref names;
+ val extend = copy;
+ fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
+ fun print _ _ = ();
+end);
+
+val _ = Context.add_setup CodegenNamesData.init;
+
+
+(* forward lookup with cache update *)
+
+fun get thy get_tabs get upd_names upd policy x =
+ let
+ val names_ref = CodegenNamesData.get thy
+ val (Names names) = ! names_ref;
+ fun mk_unique used name =
+ let
+ fun mk_name 0 = name
+ | mk_name i = name ^ "_" ^ string_of_int i
+ fun find_name i =
+ let
+ val name = mk_name i
+ in
+ if used name
+ then find_name (i+1)
+ else name
+ end;
+ val name = find_name 0;
+ in name end;
+ val tabs = get_tabs names;
+ fun declare name =
+ let
+ val names' = upd_names (K (upd (x, name) (fst tabs),
+ Symtab.update_new (name, x) (snd tabs))) (Names names)
+ in (names_ref := names'; name) end;
+ in case get (fst tabs) x
+ of SOME name => name
+ | NONE => let
+ val used = Symtab.defined (snd tabs);
+ val raw_name = policy thy x;
+ val name = mk_unique used raw_name;
+ in declare name end
+ end;
+
+
+(* backward lookup *)
+
+fun rev thy get_tabs errname name =
+ let
+ val names_ref = CodegenNamesData.get thy
+ val (Names names) = ! names_ref;
+ val tab = (snd o get_tabs) names;
+ in case Symtab.lookup tab name
+ of SOME x => x
+ | NONE => error ("no such " ^ errname ^ ": " ^ quote name)
+ end;
+
+
+(* theory name lookup *)
+
+fun thyname_of thy f errmsg x =
+ let
+ fun thy_of thy =
+ if f thy x then case get_first thy_of (Theory.parents_of thy)
+ of NONE => SOME thy
+ | thy => thy
+ else NONE;
+ in case thy_of thy
+ of SOME thy => Context.theory_name thy
+ | NONE => error (errmsg x) end;
+
+fun thyname_of_class thy =
+ thyname_of thy (fn thy => member (op =) (Sign.classes thy))
+ (fn class => "thyname_of_class: no such class: " ^ quote class);
+
+fun thyname_of_tyco thy =
+ thyname_of thy Sign.declared_tyname
+ (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
+
+fun thyname_of_instance thy =
+ let
+ fun test_instance thy (class, tyco) =
+ can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+ in thyname_of thy test_instance
+ (fn (class, tyco) => "thyname_of_instance: no such instance: " ^ quote class ^ ", " ^ quote tyco)
+ end;
+
+fun thyname_of_const thy =
+ thyname_of thy Sign.declared_const
+ (fn c => "thyname_of_const: no such constant: " ^ quote c);
+
+
+(* dissolving of ad-hoc overloading *)
+
+fun typinst_of_typ thy (c, ty) =
+ let
+ fun disciplined _ [(Type (tyco, _))] =
+ [Type (tyco, map (fn v => TFree (v, Sign.defaultS thy)) (*for monotonicity*)
+ (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]
+ | disciplined sort _ =
+ [TFree ("'a", sort)];
+ fun ad_hoc c tys =
+ let
+ val def_tyinsts =
+ map (#lhs o snd) (Defs.specifications_of (Theory.defs_of thy) c);
+ val tyinst = find_first
+ (fn tys' => forall (Sign.typ_instance thy) (tys' ~~ tys)) def_tyinsts;
+ in case tyinst
+ of SOME tys => tys
+ | NONE => Consts.typargs (Sign.consts_of thy)
+ (c, (Logic.unvarifyT o Sign.the_const_type thy) c)
+ end;
+ val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty);
+ in if c = "op =" then (c, disciplined (Sign.defaultS thy) tyinsts)
+ else case AxClass.class_of_param thy c
+ of SOME class => (c, disciplined [class] tyinsts)
+ | _ => (c, ad_hoc c tyinsts)
+ end;
+
+fun get_overl_def_module thy ("op =", [Type (tyco, _)]) =
+ SOME (thyname_of_tyco thy tyco)
+ | get_overl_def_module thy (c, tys) =
+ get_first (fn (_, { lhs, module, ...}) =>
+ if forall (Sign.typ_instance thy) (lhs ~~ tys) then SOME module else NONE)
+ (Defs.specifications_of (Theory.defs_of thy) c);
+
+fun typ_of_typinst thy (c, tys) =
+ (c, Consts.instance (Sign.consts_of thy) (c, tys));
+
+
+(* purification of identifiers *)
+
+val purify_name =
+ let
+ fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
+ val is_junk = not o is_valid andf Symbol.not_eof;
+ val junk = Scan.any is_junk;
+ val scan_valids = Symbol.scanner "Malformed input"
+ ((junk |--
+ (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode)
+ --| junk))
+ -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::);
+ in explode #> scan_valids #> space_implode "_" end;
+
+fun purify_op "0" = "zero"
+ | purify_op "1" = "one"
+ | purify_op s =
+ let
+ fun rep_op "+" = SOME "sum"
+ | rep_op "-" = SOME "diff"
+ | rep_op "*" = SOME "prod"
+ | rep_op "/" = SOME "quotient"
+ | rep_op "&" = SOME "conj"
+ | rep_op "|" = SOME "disj"
+ | rep_op "=" = SOME "eq"
+ | rep_op "~" = SOME "inv"
+ | rep_op "@" = SOME "append"
+ | rep_op s = NONE;
+ val scan_valids = Symbol.scanner "Malformed input"
+ (Scan.repeat (Scan.some rep_op || Scan.one (K true)));
+ in (explode #> scan_valids #> implode) s end;
+
+val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode;
+val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
+
+fun purify_var v =
+ if nth (explode v) 0 = "'"
+ then "'" ^ (purify_name #> purify_lower #> unprefix "'") v
+ else (purify_name #> purify_lower) v;
+
+val purify_idf = purify_op #> purify_name;
+val purify_prefix = map (purify_idf #> purify_upper);
+val purify_base = purify_idf #> purify_lower;
+
+
+(* explicit given constant names with cache update *)
+
+fun force (c_ty, 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 = CodegenNamesData.get thy;
+ val (Names names) = ! names_ref;
+ val (const, constrev) = #const names;
+ val c_tys as (c, _) = typinst_of_typ thy c_ty;
+ val _ = if Consttab.defined const c_tys
+ then error ("constant already named: " ^
+ quote (c ^ "::" ^ (Sign.string_of_typ thy o snd o typ_of_typinst thy) c_tys))
+ else ();
+ val _ = if Symtab.defined constrev name
+ then error ("name already given to constant: " ^ 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);
+ in
+ thy
+ end;
+
+
+(* naming policies *)
+
+fun policy thy get_basename get_thyname name =
+ let
+ val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name;
+ val base = (purify_base o get_basename) name;
+ in NameSpace.pack (prefix @ [base]) end;
+
+fun class_policy thy = policy thy NameSpace.base thyname_of_class;
+fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
+fun instance_policy thy = policy thy (fn (class, tyco) =>
+ NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
+
+fun const_policy thy (c, tys) =
+ case get_overl_def_module thy (c, tys)
+ of NONE => policy thy NameSpace.base thyname_of_const c
+ | SOME thyname => let
+ val prefix = (purify_prefix o NameSpace.unpack) thyname;
+ val base = (purify_base o NameSpace.base) c;
+ val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
+ val base' = space_implode "_" (base :: tycos);
+ in NameSpace.pack (prefix @ [base']) end;
+
+
+(* external interfaces *)
+
+fun class thy =
+ get thy #class Symtab.lookup map_class Symtab.update class_policy;
+fun tyco thy =
+ get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy;
+fun instance thy =
+ get thy #instance Insttab.lookup map_inst Insttab.update instance_policy;
+fun const thy =
+ get thy #const Consttab.lookup map_const Consttab.update const_policy
+ o typinst_of_typ thy;
+
+fun class_rev thy = rev thy #class "class";
+fun tyco_rev thy = rev thy #tyco "type constructor";
+fun instance_rev thy = rev thy #instance "instance";
+fun const_rev thy = rev thy #const "constant" #> typ_of_typinst thy;
+
+
+(* reading constants as terms *)
+
+fun read_const_typ thy raw_t =
+ let
+ val t = Sign.read_term thy raw_t
+ in case try dest_Const t
+ of SOME c_ty => c_ty
+ | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
+ end;
+
+fun read_const thy =
+ const thy o read_const_typ thy;
+
+
+(* outer syntax *)
+
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+fun force_e (raw_c, name) thy =
+ force (read_const_typ thy raw_c, name) thy;
+
+val constnameK = "code_constname";
+
+val constnameP =
+ OuterSyntax.command constnameK "declare code name for constant" K.thy_decl (
+ P.term -- P.name
+ >> (fn (raw_c, name) =>
+ Toplevel.theory (force_e (raw_c, name)))
+ );
+
+in
+
+val _ = OuterSyntax.add_parsers [constnameP];
+
+
+end; (*local*)
+
+end;
--- a/src/Pure/Tools/codegen_package.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Aug 08 08:19:30 2006 +0200
@@ -29,7 +29,7 @@
val add_appconst: xstring * appgen -> theory -> theory;
val add_appconst_i: string * appgen -> theory -> theory;
val appgen_default: appgen;
- val appgen_number_of: (theory -> term -> IntInf.int) -> appgen;
+ val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen;
val appgen_char: (term -> int option) -> appgen;
val appgen_case: (theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option)
@@ -46,7 +46,7 @@
structure DatatypeconsNameMangler: NAME_MANGLER;
structure CodegenData: THEORY_DATA;
type auxtab;
- val mk_tabs: theory -> string list option -> auxtab;
+ val mk_tabs: theory -> string list option -> (string * typ) list -> auxtab;
val alias_get: theory -> string -> string;
val idf_of_name: theory -> string -> string -> string;
val idf_of_const: theory -> auxtab -> string * typ -> string;
@@ -143,8 +143,6 @@
(* code generator basics *)
-type deftab = (typ * thm) list Symtab.table;
-
fun is_overloaded thy c = case Theory.definitions_of thy c
of [] => true (* FIXME false (!?) *)
| [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
@@ -231,7 +229,7 @@
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
);
-type auxtab = (bool * string list option * deftab)
+type auxtab = (bool * string list option * CodegenTheorems.thmtab)
* ((InstNameMangler.T * string Symtab.table Symtab.table) * (typ list Symtab.table * ConstNameMangler.T)
* DatatypeconsNameMangler.T);
type eqextr = theory -> auxtab
@@ -392,9 +390,9 @@
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_co thy (tabs as (_, (_, _, dtcontab))) (co, dtco) =
- case CodegenTheorems.get_datatypes thy dtco
- of SOME ((_, cos), _) => if AList.defined (op =) cos co
+fun idf_of_co thy (tabs as ((_, _, thmtab), (_, _, dtcontab))) (co, dtco) =
+ case CodegenTheorems.get_dtyp_spec thmtab 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
@@ -496,7 +494,7 @@
of NONE => []
| SOME (f, _) => f thy;
-fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
+fun const_of_idf thy (tabs as ((_, _, thmtab), (_, _, dtcontab))) idf =
case recconst_of_idf thy tabs idf
of SOME c_ty => SOME c_ty
| NONE => case dest_nsp nsp_mem idf
@@ -522,7 +520,7 @@
| check_strict thy f x ((true, _, _), _) =
true;
-fun no_strict ((_, targets, deftab), tabs') = ((false, targets, deftab), tabs');
+fun no_strict ((_, targets, thmtab), tabs') = ((false, targets, thmtab), tabs');
fun ensure_def_class thy tabs cls trns =
let
@@ -552,15 +550,15 @@
|> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls'
|> pair cls'
end
-and ensure_def_tyco thy tabs tyco trns =
+and ensure_def_tyco thy (tabs as ((_, _, thmtab), _)) tyco trns =
let
val tyco' = idf_of_name thy nsp_tyco tyco;
val strict = check_strict thy #syntax_tyco tyco' tabs;
fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
case name_of_idf thy nsp_tyco dtco
of SOME dtco =>
- (case CodegenTheorems.get_datatypes thy dtco
- of SOME ((vars, cos), _) =>
+ (case CodegenTheorems.get_dtyp_spec thmtab dtco
+ of SOME (vars, cos) =>
trns
|> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
|> fold_map (exprgen_tyvar_sort thy tabs) vars
@@ -611,8 +609,8 @@
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 (c, ty) trns =
- case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty) (* FIXME *)
+and mk_fun thy (tabs as ((_, _, thmtab), _)) (c, ty) trns =
+ case CodegenTheorems.get_fun_thms thmtab (c, Logic.legacy_varifyT ty) (*FIXME*)
of eq_thms as eq_thm :: _ =>
let
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
@@ -706,7 +704,7 @@
|> mk_fun thy tabs (c, ty)
|-> (fn SOME (funn, _) => succeed (Fun funn)
| NONE => fail ("no defining equations found for " ^
- (quote o Display.raw_string_of_term o Const) (c, ty)))
+ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))))
| NONE =>
trns
|> fail ("not a constant: " ^ quote c);
@@ -742,7 +740,7 @@
val strict = check_strict thy #syntax_const idf tabs;
in
trns
- |> debug_msg (fn _ => "generating constant " ^ (quote o Display.raw_string_of_term o Const) (c, ty))
+ |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))
|> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
|> pair idf
end
@@ -816,16 +814,16 @@
(* parametrized generators, for instantiation in HOL *)
-fun appgen_number_of int_of_bin thy tabs (app as (c as (_, ty), [bin])) trns =
- case try (int_of_bin thy) bin
- of SOME i => if i < 0 then error ("negative numeral: " ^ IntInf.toString i)
- (*preprocessor eliminates nat and negative numerals*)
+fun appgen_rep_bin int_of_numeral thy tabs (app as (c as (_, ty), [bin])) trns =
+ case try (int_of_numeral thy) bin
+ of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
+ trns
+ |> appgen_default thy (no_strict tabs) app
else
trns
- |> pair (CodegenThingol.INum (i, IVar ""))
- (*|> exprgen_term thy (no_strict tabs) (Const c)
+ |> exprgen_term thy (no_strict tabs) (Const c)
||>> exprgen_term thy (no_strict tabs) bin
- |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))*)
+ |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
| NONE =>
trns
|> appgen_default thy tabs app;
@@ -890,7 +888,7 @@
(** theory interface **)
-fun mk_tabs thy targets =
+fun mk_tabs thy targets cs =
let
fun mk_insttab thy =
let
@@ -966,7 +964,7 @@
val insttab = mk_insttab thy;
val overltabs = mk_overltabs thy;
val dtcontab = mk_dtcontab thy;
- in ((true, targets, Symtab.empty), (insttab, overltabs, dtcontab)) end;
+ in ((true, targets, CodegenTheorems.mk_thmtab thy cs), (insttab, overltabs, dtcontab)) end;
fun get_serializer target =
case Symtab.lookup (!serializers) target
@@ -992,12 +990,12 @@
map_module (purge idfs) thy
end;*)
-fun expand_module targets init gen arg thy =
+fun expand_module targets cs init gen arg thy =
thy
|> CodegenTheorems.notify_dirty
|> `(#modl o CodegenData.get)
|> (fn (modl, thy) =>
- (start_transact init (gen thy (mk_tabs thy targets) arg) modl, thy))
+ (start_transact init (gen thy (mk_tabs thy targets cs) arg) modl, thy))
|-> (fn (x, modl) => map_module (K modl) #> pair x);
fun rename_inconsistent thy =
@@ -1024,17 +1022,26 @@
else add_alias (src, dst) thy
in fold add inconsistent thy end;
+fun consts_of t =
+ fold_aterms (fn Const c => cons c | _ => I) t [];
+
fun codegen_term t thy =
- thy
- |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) NONE exprgen_term t;
+ let
+ val _ = Thm.cterm_of thy t;
+(* val _ = writeln "STARTING GENERATION"; *)
+(* val _ = (writeln o Sign.string_of_term thy) t; *)
+ in
+ thy
+ |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) (consts_of t) NONE exprgen_term t
+ end;
val is_dtcon = has_nsp nsp_dtcon;
fun consts_of_idfs thy =
- map (the o const_of_idf thy (mk_tabs thy NONE));
+ map (the o const_of_idf thy (mk_tabs thy NONE []));
-fun idfs_of_consts thy =
- map (idf_of_const thy (mk_tabs thy NONE));
+fun idfs_of_consts thy cs =
+ map (idf_of_const thy (mk_tabs thy NONE cs)) cs;
fun get_root_module thy =
thy
@@ -1083,11 +1090,16 @@
| NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
end;
-fun read_quote get reader gen raw thy =
- thy
- |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) ((SOME o get) thy)
- (fn thy => fn tabs => gen thy tabs o single o reader thy) raw
- |-> (fn [x] => pair x);
+fun read_quote get reader consts_of gen raw thy =
+ let
+ val it = reader thy raw;
+ val cs = consts_of it;
+ in
+ thy
+ |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) cs ((SOME o get) thy)
+ (fn thy => fn tabs => gen thy tabs) [it]
+ |-> (fn [x] => pair x)
+ end;
fun gen_add_syntax_class prep_class class target pretty thy =
thy
@@ -1138,7 +1150,7 @@
end;
in
CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
- (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ
+ (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ (K [])
(fn thy => fn tabs => fold_map (exprgen_type thy tabs)))
#-> (fn reader => pair (mk reader))
end;
@@ -1159,7 +1171,9 @@
fun parse_syntax_const raw_const =
let
fun prep_const thy raw_const =
- idf_of_const thy (mk_tabs thy NONE) (read_const thy raw_const);
+ let
+ val c_ty = read_const thy raw_const
+ in idf_of_const thy (mk_tabs thy NONE [c_ty]) c_ty end;
fun no_args_const thy raw_const =
(length o fst o strip_type o snd o read_const thy) raw_const;
fun mk reader target thy =
@@ -1173,7 +1187,7 @@
end;
in
CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
- (read_quote (fn thy => prep_const thy raw_const) Sign.read_term
+ (read_quote (fn thy => prep_const thy raw_const) Sign.read_term consts_of
(fn thy => fn tabs => fold_map (exprgen_term thy tabs)))
#-> (fn reader => pair (mk reader))
end;
@@ -1181,17 +1195,21 @@
fun add_pretty_list raw_nil raw_cons (target, seri) thy =
let
val _ = get_serializer target;
- val tabs = mk_tabs thy NONE;
- fun mk_const raw_name =
+ fun prep_const raw =
let
- val name = Sign.intern_const thy raw_name;
- in idf_of_const thy tabs (name, Sign.the_const_type thy name) end;
- val nil' = mk_const raw_nil;
- val cons' = mk_const raw_cons;
- val pr' = CodegenSerializer.pretty_list nil' cons' seri;
+ val c = Sign.intern_const thy raw
+ in (c, Sign.the_const_type thy c) end;
+ val nil' = prep_const raw_nil;
+ val cons' = prep_const raw_cons;
+ val tabs = mk_tabs thy NONE [nil', cons'];
+ fun mk_const c_ty =
+ idf_of_const thy tabs c_ty;
+ val nil'' = mk_const nil';
+ val cons'' = mk_const cons';
+ val pr = CodegenSerializer.pretty_list nil'' cons'' seri;
in
thy
- |> add_pretty_syntax_const cons' target pr'
+ |> add_pretty_syntax_const cons'' target pr
end;
@@ -1212,7 +1230,7 @@
val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => ();
in
thy
- |> expand_module targets NONE (fold_map oo ensure_def_const) consts
+ |> expand_module targets consts NONE (fold_map oo ensure_def_const) consts
|-> (fn cs => pair (SOME cs))
end
| generate_code _ NONE thy =
--- a/src/Pure/Tools/codegen_serializer.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Aug 08 08:19:30 2006 +0200
@@ -746,11 +746,13 @@
in
mk_memdefs (map from_supclass suparities) memdefs |> SOME
end
- | ml_from_def (name, CodegenThingol.Classinstmember) = NONE;
+ | ml_from_def (name, CodegenThingol.Classinstmember) = NONE
+ | ml_from_def (name, def) = error ("illegal definition for " ^ quote name ^ ": " ^
+ (Pretty.output o CodegenThingol.pretty_def) def);
in case defs
- of (_, CodegenThingol.Fun _)::_ => (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs
- | (_, CodegenThingol.Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
- | (_, CodegenThingol.Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+ of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
+ | (_, CodegenThingol.Datatypecons _)::_ => ((*writeln "DTCO";*) (SOME o ml_from_datatypes o filter_datatype) defs)
+ | (_, CodegenThingol.Datatype _)::_ => ((*writeln "DT";*) (SOME o ml_from_datatypes o filter_datatype) defs)
| (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
| (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
| [def] => ml_from_def def
--- a/src/Pure/Tools/codegen_theorems.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Tue Aug 08 08:19:30 2006 +0200
@@ -24,12 +24,11 @@
val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
val preprocess: theory -> thm list -> thm list;
- val get_funs: theory -> string * typ -> thm list;
val get_datatypes: theory -> string
-> (((string * sort) list * (string * typ list) list) * thm list) option;
type thmtab;
- val mk_thmtab: (string * typ) list -> theory -> thmtab * theory;
+ val mk_thmtab: theory -> (string * typ) list -> thmtab;
val norm_typ: theory -> string * typ -> string * typ;
val get_sortalgebra: thmtab -> Sorts.algebra;
val get_dtyp_of_cons: thmtab -> string * typ -> string option;
@@ -42,7 +41,8 @@
val init_obj: (thm * thm) * (thm * thm) -> theory -> theory;
val debug: bool ref;
val debug_msg: ('a -> string) -> 'a -> 'a;
-
+ structure ConstTab: TABLE;
+ structure ConstGraph: GRAPH;
end;
structure CodegenTheorems: CODEGEN_THEOREMS =
@@ -412,7 +412,7 @@
(*) *) @ [
Pretty.fbrk,
Pretty.block (
- Pretty.str "unfolding theorems:"
+ Pretty.str "inlined theorems:"
:: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_thm) unfolds
)])
@@ -610,6 +610,7 @@
#> Drule.zero_var_indexes
)
|> drop_redundant thy
+ |> debug_msg (fn _ => "[cg_thm] preprocessing done")
end;
@@ -635,7 +636,7 @@
Theory.definitions_of thy c
|> debug_msg (fn _ => "[cg_thm] trying spec")
(* FIXME avoid dynamic name space lookup!? (via Thm.get_axiom_i etc.??) *)
- |> maps (PureThy.get_thms thy o Name o #name)
+ |> maps (fn { name, ... } => these (try (PureThy.get_thms thy) (Name name)))
|> map_filter (try (dest_fun thy))
|> filter_typ;
in
@@ -693,6 +694,33 @@
| _ => []
else [];
+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;
+
structure ConstTab = TableFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
structure ConstGraph = GraphFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
@@ -729,14 +757,10 @@
fun get_fun_thms (thy, (fungr, _), _) (c, ty) =
let
val (_, ty') = norm_typ thy (c, ty);
- in these (try (ConstGraph.get_node fungr) (c, ty')) end;
+ in these (try (ConstGraph.get_node fungr) (c, ty')) |> check_thms c end;
-fun mk_thmtab' thy cs =
+fun mk_thmtab thy cs =
let
- fun get_dtco_candidate ty =
- case strip_type ty
- of (_, Type (tyco, _)) => SOME tyco
- | _ => NONE;
fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
| add_tycos _ = I;
val add_consts = fold_aterms
@@ -745,7 +769,7 @@
fun add_dtyps_of_type ty thmtab =
let
val tycos = add_tycos ty [];
- val tycos_new = filter (is_some o get_dtyp_spec thmtab) tycos;
+ val tycos_new = filter (is_none o get_dtyp_spec thmtab) tycos;
fun add_dtyp_spec dtco (dtyp_spec as (vs, cs)) ((thy, (fungr, dtcotab), (algebra, dttab))) =
let
fun mk_co (c, tys) =
@@ -777,66 +801,14 @@
val (_, ty') = norm_typ thy (c, ty);
in
thmtab
- |> add_dtyps_of_type ty
- |> add_funthms (c, ty)
- end;
- fun narrow_typs fungr =
- let
- (*
- (*!!!remember whether any instantiation had been applied!!!*)
- fun narrow_thms insts thms =
- let
- val (c_def, ty_def) =
- (norm_typ thy o dest_Const o fst o Logic.dest_equals o Thm.prop_of o hd) thms;
- val cs = fold (add_consts o snd o Logic.dest_equals o Thm.prop_of) thms [];
- fun eval_inst c (inst, ty) =
- let
- val inst_ctxt = Sign.const_typargs thy (c, ty);
- val inst_zip = fold (fn (v, ty) => (ty, (the o AList.lookup (op =) inst_ctxt) v)) inst
- fun add_inst (ty_inst, ty_ctxt) =
- if Sign.typ_instance thy (ty_inst, ty_ctxt)
- then I
- else Sign.typ_match thy (ty_ctxt, ty_inst);
- in fold add_inst inst_zip end;
- val inst =
- Vartab.empty
- |> fold (fn c_ty as (c, ty) =>
- case ConstTab.lookup insts (norm_typ thy c_ty)
- of NONE => I
- | SOME inst => eval_inst c (inst, ty)) cs
- |> Vartab.dest
- |> map (fn (v, (_, ty)) => (v, ty));
- val instT = map (fn (v, ty) =>
- (Thm.ctyp_of thy (TVar v, Thm.ctyp_of thy ty))) inst;
- val thms' =
- if null inst then NONE thms else
- map Thm.instantiate (instT, []) thms;
- val inst' = if null inst then NONE
- else SOME inst;
- in (inst', thms') end;
- fun narrow_css [c] (insts, fungr) =
- (* HIER GEHTS WEITER *)
- (insts, fungr)
- | narrow_css css (insts, fungr) =
- (insts, fungr)
- *)
- val css = rev (Graph.strong_conn fungr);
- in
- (ConstTab.empty, fungr)
- (*|> fold narrow_css css*)
- |> snd
+ |> add_dtyps_of_type ty'
+ |> add_funthms (c, ty')
end;
in
thmtab_empty thy
|> fold add_c cs
-(* |> (apfst o apfst) narrow_typs *)
end;
-fun mk_thmtab cs thy =
- thy
- |> get_reset_dirty
- |> snd
- |> `(fn thy => mk_thmtab' thy cs);
(** code attributes and setup **)
@@ -848,9 +820,10 @@
in
val _ = map (Context.add_setup o add_simple_attribute) [
("fun", add_fun),
+ ("nofun", del_fun),
("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
("inline", add_unfold),
- ("nofold", del_unfold)
+ ("noinline", del_unfold)
]
end; (*local*)
--- a/src/Pure/Tools/codegen_thingol.ML Tue Aug 08 08:19:18 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Aug 08 08:19:30 2006 +0200
@@ -305,8 +305,8 @@
f e
| map_pure f (e as _ `|-> _) =
f e
- | map_pure _ (INum _) =
- error ("sorry, no pure representation for numerals so far")
+ | map_pure f (INum (_, e0)) =
+ f e0
| map_pure f (IChar (_, e0)) =
f e0
| map_pure f (ICase (_, e0)) =
@@ -808,10 +808,10 @@
@ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls
end;
val names = subtract (op =) hidden (allnames modl);
- (*val _ = writeln "HIDDEN";
- val _ = (writeln o commas) hidden;
- val _ = writeln "NAMES";
- val _ = (writeln o commas) names;*)
+(* val _ = writeln "HIDDEN"; *)
+(* val _ = (writeln o commas) hidden; *)
+(* val _ = writeln "NAMES"; *)
+(* val _ = (writeln o commas) names; *)
fun is_bot name =
case get_def modl name of Bot => true | _ => false;
val bots = filter is_bot names;
@@ -825,10 +825,10 @@
val selected = subtract (op =) bots' names;
(* val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y) *)
val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest);
- (*val _ = writeln "SELECTED";
+(* val _ = writeln "SELECTED";
val _ = (writeln o commas) selected;
val _ = writeln "DEPS";
- val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps;*)
+ val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps; *)
in
empty_module
|> fold (fn name => add_def (name, get_def modl name)) selected